minor fixes

crucible-llvm/crucible-llvm.cabal

@@ -23,6 +23,7 @@ library
  directory,
  ghc-prim,
  extra,
+ filepath,
  hashable,
  hashtables,
  lens,

crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs

@@ -94,6 +94,7 @@ import Data.Maybe
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import qualified Data.Text as Text
+import System.FilePath
 
 import qualified Text.LLVM.AST as L
 
@@ -247,8 +248,10 @@ setLocation (x:xs) =
 
  where
  getFile = Text.pack . maybe "" filenm . findFile
- filenm di = L.difDirectory di ++ "/" ++ L.difFilename di
 
+ filenm di
+ | isRelative (L.difFilename di) = L.difDirectory di </> L.difFilename di
+ | otherwise = L.difFilename di
 
 findFile :: (?lc :: TypeContext) => L.ValMd -> Maybe L.DIFile
 findFile (L.ValMdRef x) = findFile =<< lookupMetadata x

crucible/src/Lang/Crucible/Simulator/EvalStmt.hs

@@ -62,7 +62,6 @@ import What4.InterpretedFloatingPoint (freshFloatConstant)
 import What4.Partial
 import What4.ProgramLoc
 import What4.Symbol (emptySymbol)
-import What4.Utils.StringLiteral
 
 import Lang.Crucible.Backend
 import Lang.Crucible.CFG.Core

crux/src/Crux/Config/Common.hs

@@ -77,6 +77,9 @@ data CruxOptions = CruxOptions
  -- ^ Should the MC-SAT Yices solver be enabled (disables unsat cores; default: no)
  , floatMode :: String
  -- ^ Tells the solver which representation to use for floating point values.
+
+ , proofGoalsFailFast :: Bool
+ -- ^ If true, stop attempting to prove goals as soon as one is disproved
  }
 
 
@@ -152,6 +155,10 @@ cruxOptions = Config
  ++ " i.e. one of [real|ieee|uninterpreted|default].\n"
  ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
 
+ proofGoalsFailFast <-
+ section "proof-goals-fail-fast" yesOrNoSpec False
+ "If true, stop attempting to prove goals as soon as one of them is disproved"
+
  pure CruxOptions { .. }
 
 
@@ -231,6 +238,10 @@ cruxOptions = Config
  "Enable the MC-SAT solver in Yices (disables unsat cores)"
  $ NoArg $ \opts -> Right opts { yicesMCSat = True }
 
+ , Option [] ["fail-fast"]
+ "Stop attempting to prove goals as soon as one of them is disproved"
+ $ NoArg $ \opts -> Right opts { proofGoalsFailFast = True }
+
  , Option "f" ["floating-point"]
  ("Select floating point representation,"
  ++ " i.e. one of [real|ieee|uninterpreted|default].\n"

crux/src/Crux/Goal.hs

@@ -5,7 +5,7 @@
 module Crux.Goal where
 
 import Control.Lens ((^.), view)
-import Control.Monad (forM_, unless)
+import Control.Monad (forM_, unless, when)
 import Data.Either (partitionEithers)
 import Data.IORef
 import Data.Maybe (fromMaybe)
@@ -116,16 +116,18 @@ proveGoals opts _ctxt Nothing =
 proveGoals opts ctxt (Just gs0) =
  do let sym = ctxt ^. ctxSymInterface
  sp <- getSolverProcess sym
- goalNum <- newIORef (0,0) -- total, proved
+ goalNum <- newIORef (0,0,0) -- total, proved, disproved
  nameMap <- newIORef Map.empty
  unless hasUnsatCores $
  sayWarn "Crux" "Warning: skipping unsat cores because MC-SAT is enabled."
  res <- inNewFrame sp (go sp goalNum gs0 nameMap)
- (tot,proved) <- readIORef goalNum
+ (tot,proved,disproved) <- readIORef goalNum
  if proved /= tot
  then sayFail "Crux" $ unwords
- [ "Failed to prove", show (tot - proved)
- , "out of", show tot, "goals." ]
+ [ "Disproved", show disproved
+ , "out of", show tot, "goals."
+ , show (tot - proved - disproved), "goals are unknown."
+ ]
  else sayOK "Crux" $ unwords [ "Proved all", show tot, "goals." ]
  return (Just res)
  where
@@ -135,6 +137,8 @@ proveGoals opts ctxt (Just gs0) =
 
  hasUnsatCores = not (yicesMCSat opts)
 
+ failfast = proofGoalsFailFast opts
+
  go sp gn gs nameMap = do
  case gs of
 
@@ -147,7 +151,7 @@ proveGoals opts ctxt (Just gs0) =
  return (Assuming ps res)
 
  Prove p ->
- do num <- atomicModifyIORef' gn (\(val,y) -> ((val + 1,y), val))
+ do num <- atomicModifyIORef' gn (\(val,y,z) -> ((val + 1,y,z), val))
  start num
  let sym = ctxt ^. ctxSymInterface
  nm <- doAssume =<< mkFormula conn =<< notPred sym (p ^. labeledPred)
@@ -156,15 +160,17 @@ proveGoals opts ctxt (Just gs0) =
  res <- check sp "proof"
  ret <- case res of
  Unsat () ->
- do modifyIORef' gn (\(x,f) -> (x,f+1))
+ do modifyIORef' gn (\(x,u,s) -> (x,u+1,s))
  namemap <- readIORef nameMap
  core <- if hasUnsatCores
  then map (lookupnm namemap) <$> getUnsatCore sp
  else return (Map.elems namemap)
  return (Prove (p, (Proved core)))
 
  Sat () ->
- do f <- smtExprGroundEvalFn conn (solverEvalFuns sp)
+ do modifyIORef' gn (\(x,u,s) -> (x,u,s+1))
+ when failfast (sayOK "Crux" "Counterexample found, skipping remaining goals.")
+ f <- smtExprGroundEvalFn conn (solverEvalFuns sp)
  let model = ctxt ^. cruciblePersonality
  vals <- evalModel f model
  return (Prove (p, NotProved (Just (ModelView vals))))
@@ -177,8 +183,15 @@ proveGoals opts ctxt (Just gs0) =
  do g1' <- inNewFrame sp (go sp gn g1 nameMap)
  -- NB, we don't need 'inNewFrame' here because
  -- we don't need to back up to this point again.
- g2' <- go sp gn g2 nameMap
- return (ProveConj g1' g2')
+
+ if failfast then
+ do (_,_,s) <- readIORef gn
+ if s > 0 then
+ return g1'
+ else
+ ProveConj g1' <$> go sp gn g2 nameMap
+ else
+ ProveConj g1' <$> go sp gn g2 nameMap
 
  where
  conn = solverConn sp

what4/src/What4/Interface.hs

@@ -537,7 +537,6 @@ class (IsExpr (SymExpr sym), HashableF (SymExpr sym)) => IsExprBuilder sym where
 
  -- | Equality of boolean values
  eqPred :: sym -> Pred sym -> Pred sym -> IO (Pred sym)
- eqPred sym x y = notPred sym =<< xorPred sym x y
 
  -- | If-then-else on a predicate.
  itePred :: sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)

what4/src/What4/Protocol/SMTLib2/Syntax.hs

@@ -679,7 +679,7 @@ bvashr = bin_app "bvashr"
 --
 -- Note. This is in @QF_BV@, but not the bitvector theory.
 bvsdiv :: Term -> Term -> Term
-bvsdiv = bin_app "bvudiv"
+bvsdiv = bin_app "bvsdiv"
 
 -- | @bvsrem x y@ returns @x - y * bvsdiv x y@ when @y != 0@.
 --

what4/src/What4/Solver/Yices.hs

@@ -436,7 +436,7 @@ newConnection stream ack reqFeatures timeout bindings = do
  let nlSolver = reqFeatures `hasProblemFeature` useNonlinearArithmetic
  let features | efSolver = useLinearArithmetic
  | nlSolver = useNonlinearArithmetic .|. useIntegerArithmetic
- | otherwise = useIntegerArithmetic
+ | otherwise = yicesDefaultFeatures
  let nm | efSolver = "Yices ef-solver"
  | nlSolver = "Yices nl-solver"
  | otherwise = "Yices"