Resolve the names of terms to be held uninterpreted closer to

the SAWScript front end.

src/SAWScript/Builtins.hs

@@ -35,6 +35,8 @@ import qualified Data.ByteString.Lazy.UTF8 as B
 import qualified Data.IntMap as IntMap
 import Data.List (isPrefixOf, isInfixOf)
 import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Data.Maybe
 import Data.Time.Clock
 import Data.Typeable
@@ -472,6 +474,8 @@ printGoalSize =
      printOutLnTop Info $ "Goal unshared size: " ++ show (scTreeSize t)
      return ((), mempty, Just goal)
 
+resolveNames :: SharedContext -> [String] -> TopLevel (Set VarIndex)
+resolveNames sc nms = Set.fromList <$> mapM (resolveName sc) nms
 
 resolveName :: SharedContext -> String -> TopLevel VarIndex
 resolveName sc nm =
@@ -516,10 +520,11 @@ goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
   withFirstGoal $ \goal ->
   do sc <- getSharedContext
+     unintSet <- resolveNames sc unints
      t0 <- liftIO $ propToPredicate sc (goalProp goal)
      let gen = globalNonceGenerator
      sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen
-     (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unints t0
+     (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unintSet t0
      t1 <- liftIO $ Crucible.toSC sym p
      t2 <- liftIO $ scEqTrue sc t1
      return ((), mempty, Just (goal { goalProp = Prop t2 }))
@@ -703,11 +708,11 @@ writeSAIGComputedPrim f t n = do
 proveRME :: ProofScript SV.SatResult
 proveRME = wrapProver Prover.proveRME
 
-codegenSBV :: SharedContext -> FilePath -> [String] -> String -> TypedTerm -> IO ()
+codegenSBV :: SharedContext -> FilePath -> [String] -> String -> TypedTerm -> TopLevel ()
 codegenSBV sc path unints fname (TypedTerm _schema t) =
-  SBVSim.sbvCodeGen sc mempty unints mpath fname t
-  where mpath = if null path then Nothing else Just path
-
+  do unintSet <- resolveNames sc unints
+     let mpath = if null path then Nothing else Just path
+     io $ SBVSim.sbvCodeGen sc mempty unintSet mpath fname t
 
 -- | Bit-blast a proposition and check its validity using SBV.
 -- (Currently ignores satisfying assignments.)
@@ -720,7 +725,9 @@ proveSBV conf = proveUnintSBV conf []
 proveUnintSBV :: SBV.SMTConfig -> [String] -> ProofScript SV.SatResult
 proveUnintSBV conf unints =
   do timeout <- psTimeout <$> get
-     wrapProver (Prover.proveUnintSBV conf unints timeout)
+     sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapProver (Prover.proveUnintSBV conf unintSet timeout)
 
 applyProverToGoal :: (SharedContext
                       -> Prop -> IO (Maybe [(String, FirstOrderValue)], SolverStats))
@@ -803,40 +810,58 @@ proveUnintYices = proveUnintSBV SBV.yices
 
 --------------------------------------------------
 w4_boolector :: ProofScript SV.SatResult
-w4_boolector = wrapW4Prover $ Prover.proveWhat4_boolector []
+w4_boolector = wrapW4Prover $ Prover.proveWhat4_boolector mempty
 
 w4_z3 :: ProofScript SV.SatResult
-w4_z3 = wrapW4Prover $ Prover.proveWhat4_z3 []
+w4_z3 = wrapW4Prover $ Prover.proveWhat4_z3 mempty
 
 w4_cvc4 :: ProofScript SV.SatResult
-w4_cvc4 = wrapW4Prover $ Prover.proveWhat4_cvc4 []
+w4_cvc4 = wrapW4Prover $ Prover.proveWhat4_cvc4 mempty
 
 w4_yices :: ProofScript SV.SatResult
-w4_yices = wrapW4Prover $ Prover.proveWhat4_yices []
+w4_yices = wrapW4Prover $ Prover.proveWhat4_yices mempty
 
 w4_unint_boolector :: [String] -> ProofScript SV.SatResult
-w4_unint_boolector = wrapW4Prover . Prover.proveWhat4_boolector
+w4_unint_boolector unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_boolector unintSet)
 
 w4_unint_z3 :: [String] -> ProofScript SV.SatResult
-w4_unint_z3 = wrapW4Prover . Prover.proveWhat4_z3
+w4_unint_z3 unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_z3 unintSet)
 
 w4_unint_cvc4 :: [String] -> ProofScript SV.SatResult
-w4_unint_cvc4 = wrapW4Prover . Prover.proveWhat4_cvc4
+w4_unint_cvc4 unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_cvc4 unintSet)
 
 w4_unint_yices :: [String] -> ProofScript SV.SatResult
-w4_unint_yices = wrapW4Prover . Prover.proveWhat4_yices
+w4_unint_yices unints =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4Prover (Prover.proveWhat4_yices unintSet)
 
 offline_w4_unint_z3 :: [String] -> String -> ProofScript SV.SatResult
 offline_w4_unint_z3 unints path =
-  wrapW4ProveExporter (Prover.proveExportWhat4_z3 unints) path ".smt2"
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4ProveExporter (Prover.proveExportWhat4_z3 unintSet) path ".smt2"
 
 offline_w4_unint_cvc4 :: [String] -> String -> ProofScript SV.SatResult
 offline_w4_unint_cvc4 unints path =
-  wrapW4ProveExporter (Prover.proveExportWhat4_cvc4 unints) path ".smt2"
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4ProveExporter (Prover.proveExportWhat4_cvc4 unintSet) path ".smt2"
 
 offline_w4_unint_yices :: [String] -> String -> ProofScript SV.SatResult
 offline_w4_unint_yices unints path =
-  wrapW4ProveExporter (Prover.proveExportWhat4_yices unints) path ".smt2"
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     wrapW4ProveExporter (Prover.proveExportWhat4_yices unintSet) path ".smt2"
 
 proveWithExporter ::
   (SharedContext -> FilePath -> Prop -> IO ()) ->
@@ -870,7 +895,10 @@ offline_smtlib2 :: FilePath -> ProofScript SV.SatResult
 offline_smtlib2 path = proveWithExporter Prover.writeSMTLib2 path ".smt2"
 
 offline_unint_smtlib2 :: [String] -> FilePath -> ProofScript SV.SatResult
-offline_unint_smtlib2 unints path = proveWithExporter (Prover.writeUnintSMTLib2 unints) path ".smt2"
+offline_unint_smtlib2 unints path =
+  do sc <- lift $ SV.getSharedContext
+     unintSet <- lift $ resolveNames sc unints
+     proveWithExporter (Prover.writeUnintSMTLib2 unintSet) path ".smt2"
 
 set_timeout :: Integer -> ProofScript ()
 set_timeout to = modify (\ps -> ps { psTimeout = Just to })

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -229,7 +229,7 @@ resolveBitvectorTerm sym w tm =
      mx <- case getAllExts tm' of
              [] ->
                do -- Evaluate in SBV to test whether 'tm' is a concrete value
-                  sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty [] tm'
+                  sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty mempty tm'
                   return (SBV.svAsInteger sbv)
              _ -> return Nothing
      case mx of
@@ -245,7 +245,7 @@ resolveBoolTerm sym tm =
      mx <- case getAllExts tm' of
              [] ->
                do -- Evaluate in SBV to test whether 'tm' is a concrete value
-                  sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty [] tm'
+                  sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty mempty tm'
                   return (SBV.svAsBool sbv)
              _ -> return Nothing
      case mx of

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -360,7 +360,7 @@ resolveSAWPred cc tm = do
      mx <- case getAllExts tm' of
              [] -> do
                -- Evaluate in SBV to test whether 'tm' is a concrete value
-               sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty [] tm'
+               sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty mempty tm'
                return (SBV.svAsBool sbv)
              _ -> return Nothing
      case mx of
@@ -381,7 +381,7 @@ resolveSAWSymBV cc w tm =
      mx <- case getAllExts tm' of
              [] -> do
                -- Evaluate in SBV to test whether 'tm' is a concrete value
-               sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty [] tm'
+               sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty mempty tm'
                return (SBV.svAsInteger sbv)
              _ -> return Nothing
      case mx of

src/SAWScript/Prover/Exporter.hs

@@ -35,6 +35,7 @@ import qualified Control.Monad.Fail as Fail
 import qualified Data.AIG as AIG
 import qualified Data.ByteString as BS
 import Data.Parameterized.Nonce (globalNonceGenerator)
+import Data.Set (Set)
 import qualified Data.SBV.Dynamic as SBV
 import Text.PrettyPrint.ANSI.Leijen (vcat)
 
@@ -175,7 +176,7 @@ write_cnf sc f (TypedTerm schema t) = do
 -- | Write a proposition to an SMT-Lib version 2 file. Because @Prop@ is
 -- assumed to have universally quantified variables, it will be negated.
 writeSMTLib2 :: SharedContext -> FilePath -> Prop -> IO ()
-writeSMTLib2 sc f t = writeUnintSMTLib2 [] sc f t
+writeSMTLib2 sc f t = writeUnintSMTLib2 mempty sc f t
 
 -- | Write a @Term@ representing a predicate (i.e. a monomorphic
 -- function returning a boolean) to an SMT-Lib version 2 file. The goal
@@ -190,9 +191,9 @@ write_smtlib2 sc f (TypedTerm schema t) = do
 -- | Write a proposition to an SMT-Lib version 2 file, treating some
 -- constants as uninterpreted. Because @Prop@ is assumed to have
 -- universally quantified variables, it will be negated.
-writeUnintSMTLib2 :: [String] -> SharedContext -> FilePath -> Prop -> IO ()
-writeUnintSMTLib2 unints sc f p =
-  do (_, _, l) <- prepNegatedSBV sc unints p
+writeUnintSMTLib2 :: Set VarIndex -> SharedContext -> FilePath -> Prop -> IO ()
+writeUnintSMTLib2 unintSet sc f p =
+  do (_, _, l) <- prepNegatedSBV sc unintSet p
      let isSat = True -- l is encoded as an existential formula
      txt <- SBV.generateSMTBenchmark isSat l
      writeFile f txt

src/SAWScript/Prover/MRSolver.hs

@@ -280,7 +280,7 @@ mrProvable bool_prop =
      path_prop <- mrPathCondition <$> get
      bool_prop' <- liftSC2 scImplies path_prop bool_prop
      prop <- liftSC1 scEqTrue bool_prop'
-     (smt_res, _) <- liftSC1 (SBV.proveUnintSBV smt_conf [] timeout) (Prop prop)
+     (smt_res, _) <- liftSC1 (SBV.proveUnintSBV smt_conf mempty timeout) (Prop prop)
      case smt_res of
        Just _ -> return False
        Nothing -> return True

src/SAWScript/Prover/SBV.hs

@@ -10,6 +10,7 @@ import System.Directory
 import           Data.Maybe
 import           Data.Map ( Map )
 import qualified Data.Map as Map
+import           Data.Set ( Set )
 import qualified Data.Vector as V
 import           Control.Monad
 
@@ -32,13 +33,13 @@ import SAWScript.Prover.Rewrite(rewriteEqs)
 -- functions.
 proveUnintSBV ::
   SBV.SMTConfig {- ^ SBV configuration -} ->
-  [String]      {- ^ Uninterpreted functions -} ->
+  Set VarIndex  {- ^ Uninterpreted functions -} ->
   Maybe Integer {- ^ Timeout in milliseconds -} ->
   SharedContext {- ^ Context for working with terms -} ->
   Prop          {- ^ A proposition to be proved -} ->
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
     -- ^ (example/counter-example, solver statistics)
-proveUnintSBV conf unints timeout sc term =
+proveUnintSBV conf unintSet timeout sc term =
   do p <- findExecutable . SBV.executable $ SBV.solver conf
      unless (isJust p) . fail $ mconcat
        [ "Unable to locate the executable \""
@@ -47,7 +48,7 @@ proveUnintSBV conf unints timeout sc term =
        , show . SBV.name $ SBV.solver conf
        ]
 
-     (t', mlabels, lit) <- prepNegatedSBV sc unints term
+     (t', mlabels, lit) <- prepNegatedSBV sc unintSet term
 
      tp <- scWhnf sc =<< scTypeOf sc t'
      let (args, _) = asPiList tp
@@ -81,18 +82,18 @@ proveUnintSBV conf unints timeout sc term =
 -- specified function names are left uninterpreted.
 prepNegatedSBV ::
   SharedContext ->
-  [String] {- ^ Uninterpreted function names -} ->
+  Set VarIndex {- ^ Uninterpreted function names -} ->
   Prop     {- ^ Proposition to prove -} ->
   IO (Term, [Maybe SBVSim.Labeler], SBV.Symbolic SBV.SVal)
-prepNegatedSBV sc unints goal =
+prepNegatedSBV sc unintSet goal =
   do t0 <- propToPredicate sc goal
      -- Abstract over all non-function ExtCns variables
      let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
      exts <- filterM nonFun (getAllExts t0)
 
      t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
 
-     (labels, lit) <- SBVSim.sbvSolve sc mempty unints t'
+     (labels, lit) <- SBVSim.sbvSolve sc mempty unintSet t'
      let lit' = liftM SBV.svNot lit
      return (t', labels, lit')
 

src/SAWScript/Prover/What4.hs

@@ -8,6 +8,7 @@ module SAWScript.Prover.What4 where
 
 import System.IO
 
+import           Data.Set (Set)
 import qualified Data.Vector as V
 import           Control.Monad(filterM)
 import           Data.Maybe (catMaybes)
@@ -51,7 +52,7 @@ setupWhat4_sym hashConsing =
 
 proveWhat4_sym ::
   SolverAdapter St ->
-  [String] ->
+  Set VarIndex ->
   SharedContext ->
   Bool ->
   Prop ->
@@ -62,7 +63,7 @@ proveWhat4_sym solver un sc hashConsing t =
 
 proveExportWhat4_sym ::
   SolverAdapter St ->
-  [String] ->
+  Set VarIndex ->
   SharedContext ->
   Bool ->
   FilePath ->
@@ -81,7 +82,7 @@ proveExportWhat4_sym solver un sc hashConsing outFilePath t =
 
 proveWhat4_z3, proveWhat4_boolector, proveWhat4_cvc4,
   proveWhat4_dreal, proveWhat4_stp, proveWhat4_yices ::
-  [String]      {- ^ Uninterpreted functions -} ->
+  Set VarIndex  {- ^ Uninterpreted functions -} ->
   SharedContext {- ^ Context for working with terms -} ->
   Bool          {- ^ Hash-consing of What4 terms -}->
   Prop          {- ^ A proposition to be proved -} ->
@@ -96,7 +97,7 @@ proveWhat4_yices     = proveWhat4_sym yicesAdapter
 
 proveExportWhat4_z3, proveExportWhat4_boolector, proveExportWhat4_cvc4,
   proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices ::
-  [String]      {- ^ Uninterpreted functions -} ->
+  Set VarIndex  {- ^ Uninterpreted functions -} ->
   SharedContext {- ^ Context for working with terms -} ->
   Bool          {- ^ Hash-consing of ExportWhat4 terms -}->
   FilePath      {- ^ Path of file to write SMT to -}->
@@ -114,19 +115,19 @@ proveExportWhat4_yices     = proveExportWhat4_sym yicesAdapter
 setupWhat4_solver :: forall st t ff.
   SolverAdapter st   {- ^ Which solver to use -} ->
   B.ExprBuilder t st ff {- ^ The glorious sym -}  ->
-  [String]           {- ^ Uninterpreted functions -} ->
+  Set VarIndex       {- ^ Uninterpreted functions -} ->
   SharedContext      {- ^ Context for working with terms -} ->
   Prop               {- ^ A proposition to be proved/checked. -} ->
   IO ( [String]
      , [Maybe (W.Labeler (B.ExprBuilder t st ff))]
      , Pred (B.ExprBuilder t st ff)
      , SolverStats)
-setupWhat4_solver solver sym unints sc goal =
+setupWhat4_solver solver sym unintSet sc goal =
   do
      -- convert goal to lambda term
      term <- propToPredicate sc goal
      -- symbolically evaluate
-     (t', argNames, (bvs,lit0)) <- prepWhat4 sym sc unints term
+     (t', argNames, (bvs,lit0)) <- prepWhat4 sym sc unintSet term
 
      lit <- notPred sym lit0
 
@@ -142,14 +143,14 @@ setupWhat4_solver solver sym unints sc goal =
 proveWhat4_solver :: forall st t ff.
   SolverAdapter st   {- ^ Which solver to use -} ->
   B.ExprBuilder t st ff {- ^ The glorious sym -}  ->
-  [String]           {- ^ Uninterpreted functions -} ->
+  Set VarIndex       {- ^ Uninterpreted functions -} ->
   SharedContext      {- ^ Context for working with terms -} ->
   Prop               {- ^ A proposition to be proved/checked. -} ->
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
   -- ^ (example/counter-example, solver statistics)
-proveWhat4_solver solver sym unints sc goal =
+proveWhat4_solver solver sym unintSet sc goal =
   do
-     (argNames, bvs, lit, stats) <- setupWhat4_solver solver sym unints sc goal
+     (argNames, bvs, lit, stats) <- setupWhat4_solver solver sym unintSet sc goal
 
      -- log to stdout
      let logger _ str = putStrLn str
@@ -170,16 +171,16 @@ proveWhat4_solver solver sym unints sc goal =
 
 prepWhat4 ::
   forall sym. (IsSymExprBuilder sym) =>
-  sym -> SharedContext -> [String] -> Term ->
+  sym -> SharedContext -> Set VarIndex -> Term ->
   IO (Term, [String], ([Maybe (W.Labeler sym)], Pred sym))
-prepWhat4 sym sc unints t0 = do
+prepWhat4 sym sc unintSet t0 = do
   -- Abstract over all non-function ExtCns variables
   let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
   exts <- filterM nonFun (getAllExts t0)
 
   t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
 
-  (argNames, lit) <- W.w4Solve sym sc mempty unints t'
+  (argNames, lit) <- W.w4Solve sym sc mempty unintSet t'
   return (t', argNames, lit)