Add space in the Goals datatype for detailed explanations

of goal failures.

crux-llvm/src/CruxLLVMMain.hs

@@ -127,7 +127,7 @@ makeCounterExamplesLLVM opts = mapM_ go . Fold.toList
  _ -> False
 
  in case (res, skipGoal) of
- (NotProved (Just m), False) ->
+ (NotProved _ (Just m), False) ->
  do sayFail "Crux" ("Counter example for " ++ msg)
  (_prt,dbg) <- buildModelExes opts suff (ppModelC m)
  say "Crux" ("*** debug executable: " ++ dbg)

crux/src/Crux/Goal.hs

@@ -18,7 +18,7 @@ import qualified Data.Map as Map
 import qualified Data.Sequence as Seq
 import qualified Data.Text as Text
 import qualified System.Timeout as ST
-
+import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import What4.Interface (notPred, printSymExpr,asConstantPred)
 import qualified What4.Interface as WI
@@ -87,33 +87,33 @@ countDisprovedGoals gs =
  case gs of
  AtLoc _ _ gs1 -> countDisprovedGoals gs1
  Branch gs1 gs2 -> countDisprovedGoals gs1 + countDisprovedGoals gs2
- Goal _ _ _ (NotProved (Just _)) -> 1
- Goal _ _ _ (NotProved Nothing) -> 0
+ Goal _ _ _ (NotProved _ (Just _)) -> 1
+ Goal _ _ _ (NotProved _ Nothing) -> 0
  Goal _ _ _ (Proved _) -> 0
 
 countUnknownGoals :: ProvedGoals a -> Int
 countUnknownGoals gs =
  case gs of
  AtLoc _ _ gs1 -> countUnknownGoals gs1
  Branch gs1 gs2 -> countUnknownGoals gs1 + countUnknownGoals gs2
- Goal _ _ _ (NotProved Nothing) -> 1
- Goal _ _ _ (NotProved (Just _)) -> 0
+ Goal _ _ _ (NotProved _ Nothing) -> 1
+ Goal _ _ _ (NotProved _ (Just _)) -> 0
  Goal _ _ _ (Proved _) -> 0
 
 countProvedGoals :: ProvedGoals a -> Int
 countProvedGoals gs =
  case gs of
  AtLoc _ _ gs1 -> countProvedGoals gs1
  Branch gs1 gs2 -> countProvedGoals gs1 + countProvedGoals gs2
- Goal _ _ _ (NotProved _) -> 0
+ Goal _ _ _ (NotProved _ _) -> 0
  Goal _ _ _ (Proved _) -> 1
 
 countIncompleteGoals :: ProvedGoals a -> Int
 countIncompleteGoals gs =
  case gs of
  AtLoc _ _ gs1 -> countIncompleteGoals gs1
  Branch gs1 gs2 -> countIncompleteGoals gs1 + countIncompleteGoals gs2
- Goal _ (SimError _ (ResourceExhausted _), _) _ (NotProved (Just _)) -> 1
+ Goal _ (SimError _ (ResourceExhausted _), _) _ (NotProved _ (Just _)) -> 1
  Goal _ _ _ _ -> 0
 
 proveToGoal ::
@@ -125,7 +125,7 @@ proveToGoal ::
  ProvedGoals (Either AssumptionReason SimError)
 proveToGoal _ allAsmps p pr =
  case pr of
- NotProved cex -> Goal (map showLabPred allAsmps) (showLabPred p) False (NotProved cex)
+ NotProved details cex -> Goal (map showLabPred allAsmps) (showLabPred p) False (NotProved details cex)
  Proved xs ->
  let xs' = map (either (Left . (view labeledPredMsg)) (Right . (view labeledPredMsg))) xs in
  case partitionEithers xs of
@@ -219,12 +219,12 @@ proveGoalsOffline adapter opts ctx (Just gs0) = do
  when failfast $ sayOK "Crux" "Counterexample found, skipping remaining goals"
  let model = ctx ^. cruciblePersonality
  vals <- evalModel evalFn model
- return (Prove (p, NotProved (Just (ModelView vals))))
- Unknown -> return (Prove (p, NotProved Nothing))
+ return (Prove (p, NotProved mempty (Just (ModelView vals))))
+ Unknown -> return (Prove (p, NotProved mempty Nothing))
  end
  case mres of
  Just res -> return res
- Nothing -> return (Prove (p, NotProved Nothing))
+ Nothing -> return (Prove (p, NotProved mempty Nothing))
 
 
 
@@ -303,9 +303,9 @@ proveGoalsOnline sym opts ctxt (Just gs0) =
  f <- smtExprGroundEvalFn conn (solverEvalFuns sp)
  let model = ctxt ^. cruciblePersonality
  vals <- evalModel f model
- return (Prove (p, NotProved (Just (ModelView vals))))
+ return (Prove (p, NotProved (text "found counterexample!") (Just (ModelView vals))))
 
- Unknown -> return (Prove (p, NotProved Nothing))
+ Unknown -> return (Prove (p, NotProved mempty Nothing))
  end
  return ret
 

crux/src/Crux/Report.hs

@@ -100,25 +100,31 @@ jsSideCond ::
  ProofResult b ->
  JS
 jsSideCond cwd path asmps (conc,_) triv status =
- jsObj
+ jsObj $
  [ "status" ~> proved
  , "counter-example" ~> example
  , "goal" ~> jsStr goalReason
  , "location" ~> jsLoc cwd (simErrorLoc conc)
  , "assumptions" ~> jsList (map mkAsmp asmps)
  , "trivial" ~> jsBool triv
  , "path" ~> jsList path
- ]
+ ] ++ details
  where
  proved = case (status, simErrorReason conc) of
  (Proved{}, _) -> jsStr "ok"
- (NotProved _, ResourceExhausted _) -> jsStr "unknown"
- (NotProved Nothing, _) -> jsStr "unknown"
- (NotProved (Just _), _) -> jsStr "fail"
+ (NotProved _ _, ResourceExhausted _) -> jsStr "unknown"
+ (NotProved _ Nothing, _) -> jsStr "unknown"
+ (NotProved _ (Just _), _) -> jsStr "fail"
 
  example = case status of
- NotProved (Just m) -> JS (ppModelJS cwd m)
- _ -> jsNull
+ NotProved _ (Just m) -> JS (ppModelJS cwd m)
+ _ -> jsNull
+
+ details = case status of
+ Proved{} -> []
+ NotProved dets _ ->
+ let detStr = show dets in
+ if null detStr then [] else [ "goaldetails" ~> jsStr (show dets) ]
 
  mkAsmp (asmp,_) =
  jsObj [ "loc" ~> jsLoc cwd (assumptionLoc asmp)

crux/src/Crux/Types.hs

@@ -2,6 +2,7 @@
 module Crux.Types where
 
 import Data.Parameterized.Map (MapF)
+import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 
 import Lang.Crucible.Simulator.RegMap(RegValue)
 import Lang.Crucible.Simulator.OverrideSim(OverrideSim)
@@ -18,7 +19,7 @@ import Lang.Crucible.Simulator
 import Lang.Crucible.Types
 
 
--- | A simulator context 
+-- | A simulator context
 type SimCtxt sym p = SimContext (Model sym) sym p
 
 -- | The instance of the override monad we use,
@@ -56,7 +57,9 @@ data Result sym where
 
 data ProofResult a
  = Proved [a]
- | NotProved (Maybe ModelView) -- ^ Counter example, if any
+ | NotProved Doc (Maybe ModelView)
+ -- ^ Counter example, if any, and a detailed explanation of the failed goal
+
  deriving (Functor)
 
 type LPred sym = LabeledPred (Pred sym)
@@ -65,12 +68,16 @@ data ProvedGoals a =
  AtLoc ProgramLoc (Maybe ProgramLoc) (ProvedGoals a)
  | Branch (ProvedGoals a) (ProvedGoals a)
  | Goal [(AssumptionReason,String)]
- (SimError,String) Bool (ProofResult a)
+ (SimError,String)
+ Bool
+ (ProofResult a)
  -- ^ Keeps only the explanations for the relevant assumptions.
  -- The 'Maybe Int' in the assumptions corresponds to its depth in the tree
  -- (i.e., the step number, if this is a path assumption)
  -- The 'Bool' indicates if the goal is trivial (i.e., the assumptions
  -- are inconsistent)
+ -- The 'Doc' is a detailed explanation of the goal failure
+
 
 -- From Model
 
@@ -110,7 +117,3 @@ data Entry ty = Entry { entryName :: String
 -- that type for the given model, used to describe the
 -- conditions under which an SMT query is satisfiable.
 newtype ModelView = ModelView { modelVals :: MapF BaseTypeRepr Vals }
-
-
-
-

crux/src/Crux/UI/IndexHtml.hs

@@ -139,7 +139,8 @@ function drawGoals() {
  var li = $('<div/>')
  .addClass('clickable')
  .append( drawStatus(g.status)
- , $('<span/>').text(g.goal)
+ , $('<span/>').attr('title',g.goaldetails)
+ .text(g.goal)
  )
  li.click(function() {
  $('.highlight-assumed').removeClass('highlight-assumed')