Add a way do declare that names should be kept opaque during LLVM symbolic simulation

CHANGES.md

@@ -86,6 +86,10 @@ This release supports [version
 
 ## New Features
 
+* SAW has new commands `llvm_unint: [String] -> LLVMSetup ()` and
+  and analogous commands for JVM and MIR, which can be used to declare that some
+  Cryptol names should be kept opaque during symbolic simulation.
+
 * The Cryptol import syntax has been extended.
   - You can now import Cryptol module names, including qualified module
     names (which are resolved via the Cryptol load path) as well as

crucible-mir-comp/src/Mir/Compositional/State.hs

@@ -29,8 +29,15 @@ data MirState t = MirState {
   -- ^ Inforamtion about what terms are loaded
 
   mirKeepUninterp     :: IORef (Set Text),
-  -- ^ Set of names we'd like to keep uninterpreted;
-  -- we use `_cryEnv` to compute what they refer to.
+  {- ^ Set of names we'd like to keep uninterpreted;
+    we use `_cryEnv` to compute what they refer to.
+    Note that in SAW, the MIRContext has a similar field,
+    of type `Set VarIndex`. We can't do the same here, instead we keep the
+    actual `Text` names.  The reason is because `crux-mir-comp` loads Cryptol
+    code lazily, only when a function is first called.  As a result we can't
+    resolve the names early, because the Cryptol code would not yet have been
+    loaded.
+  -}
 
   mirSAWCoreState :: SAW.SAWCoreState t
 }

intTests/test2674/Example.cry

@@ -0,0 +1,7 @@
+module Example where
+
+cry_ID : [8] -> [8]
+cry_ID x = x
+
+cry_FIVE : [8] -> [8]
+cry_FIVE y = cry_ID 5 + y

intTests/test2674/example.c

@@ -0,0 +1,2 @@
+unsigned char c_ID(unsigned char x) { return x; }
+unsigned char c_FIVE(unsigned char y) { return c_ID(5)+y; }

intTests/test2674/test.saw

@@ -0,0 +1,48 @@
+m <- llvm_load_module "example.bc";
+
+import "Example.cry";
+
+thm_id <- llvm_verify
+  m "c_ID" [] false
+  do {
+    X <- llvm_fresh_var "X" (llvm_int 8);
+    llvm_execute_func [llvm_term X];
+    llvm_return (llvm_term {{ cry_ID X }} );
+  }
+  rme;
+
+fails (llvm_verify
+  m "c_FIVE" [thm_id] false
+  do {
+    Y <- llvm_fresh_var "Y" (llvm_int 8);
+    llvm_execute_func [llvm_term Y];
+    llvm_return (llvm_term {{ cry_FIVE Y }});
+  }
+  do {
+    w4_unint_rme ["cry_ID"];
+  });
+
+
+fails (llvm_verify
+  m "c_FIVE" [thm_id] false
+  do {
+    Y <- llvm_fresh_var "Y" (llvm_int 8);
+    llvm_execute_func [llvm_term Y];
+    llvm_unint ["cry_ID"];
+    llvm_return (llvm_term {{ cry_FIVE Y }});
+  }
+  do {
+    w4_unint_rme [];
+  });
+
+thm_five <- llvm_verify
+  m "c_FIVE" [thm_id] false
+  do {
+    llvm_unint ["cry_ID"];
+    Y <- llvm_fresh_var "Y" (llvm_int 8);
+    llvm_execute_func [llvm_term Y];
+    llvm_return (llvm_term {{ cry_FIVE Y }});
+  }
+  do {
+    w4_unint_rme ["cry_ID"];
+  };

intTests/test2674/test.sh

@@ -0,0 +1,2 @@
+set -e
+$SAW test.saw

intTests/test_search/search00.log.good

@@ -42,6 +42,7 @@ llvm_points_to_untyped : SetupValue -> SetupValue -> LLVMSetup ()
 llvm_postcond : Term -> LLVMSetup ()
 llvm_precond : Term -> LLVMSetup ()
 llvm_return : SetupValue -> LLVMSetup ()
+llvm_unint : [String] -> LLVMSetup ()
 llvm_unsafe_assume_spec : LLVMModule -> String -> LLVMSetup () -> TopLevel LLVMSpec
 llvm_verify : LLVMModule -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec
 19 more matches tagged experimental; use enable_experimental to see them

intTests/test_search/search01.log.good

@@ -27,6 +27,7 @@ jvm_postcond : Term -> JVMSetup ()
 jvm_precond : Term -> JVMSetup ()
 jvm_return : JVMValue -> JVMSetup ()
 jvm_static_field_is : String -> JVMValue -> JVMSetup ()
+jvm_unint : [String] -> JVMSetup ()
 jvm_unsafe_assume_spec : JavaClass -> String -> JVMSetup () -> TopLevel JVMSpec
 jvm_verify : JavaClass -> String -> [JVMSpec] -> Bool -> JVMSetup () -> ProofScript () -> TopLevel JVMSpec
 2 more matches tagged experimental; use enable_experimental to see them

saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs

@@ -1,49 +1,153 @@
 -- | Utilities for resolving 'SetupValue's that are used across language
 -- backends.
+{-# Language DataKinds, TypeOperators, GADTs, TypeApplications #-}
+{-# Language ImplicitParams #-}
 module SAWCentral.Crucible.Common.ResolveSetupValue ( 
-  resolveBoolTerm,
-  checkBooleanType
+  resolveBoolTerm, resolveBoolTerm',
+  resolveBitvectorTerm, resolveBitvectorTerm',
+  ResolveRewrite(..),
   ) where
 
+import qualified Data.Map as Map
+import           Data.Set(Set)
+import qualified Data.BitVector.Sized as BV
+import           Data.Parameterized.Some (Some(..))
+import           Data.Parameterized.NatRepr
+
 import qualified What4.BaseTypes as W4
 import qualified What4.Interface as W4
 
+
 import SAWCore.SharedTerm
+import SAWCore.Name
+import qualified SAWCore.Prim as Prim
 
 import qualified SAWCore.Simulator.Concrete as Concrete
+import qualified Lang.Crucible.Types as Crucible
+import qualified Lang.Crucible.Simulator.RegValue as Crucible
 
 import SAWCoreWhat4.ReturnTrip
 
 import SAWCentral.Crucible.Common
 
-import Cryptol.TypeCheck.Type (tIsBit)
-import CryptolSAWCore.TypedTerm (mkTypedTerm, ttType, ttIsMono)
+import SAWCentral.Proof (TheoremNonce)
+import SAWCore.Rewriter (Simpset, rewriteSharedTerm)
+import qualified CryptolSAWCore.Simpset as Cryptol
+import SAWCoreWhat4.What4(w4EvalAny, valueToSymExpr)
+
+import Cryptol.TypeCheck.Type (tIsBit, tIsSeq, tIsNum)
+import CryptolSAWCore.TypedTerm (mkTypedTerm, ttType, ttIsMono, ppTypedTermType)
 import qualified Cryptol.Utils.PP as PP
 
--- | Resolve a SAWCore 'Term' into a What4 'W4.Pred'.
-resolveBoolTerm :: Sym -> Term -> IO (W4.Pred Sym)
-resolveBoolTerm sym tm =
-  do st <- sawCoreState sym
-     let sc = saw_ctx st
-     mx <- case getAllExts tm of
-             -- concretely evaluate if it is a closed term
-             [] ->
-               do modmap <- scGetModuleMap sc
-                  let v = Concrete.evalSharedTerm modmap mempty mempty tm
-                  pure (Just (Concrete.toBool v))
-             _ -> return Nothing
-     case mx of
-       Just x  -> return (W4.backendPred sym x)
-       Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm
-
--- | Ensure that the term has Cryptol type @Bit@.
-checkBooleanType :: SharedContext -> Term -> IO ()
-checkBooleanType sc tm = do
-  tt <- mkTypedTerm sc tm
-  case ttIsMono (ttType tt) of
-    Just ty | tIsBit ty -> pure ()
-            | otherwise -> fail $ unlines
-                 [ "Expected type: Bit"
-                 , "Actual type:   " ++ show (PP.pp ty)
-                 ]
-    Nothing -> fail "Expected monomorphic Cryptol type, got polymorphic or unrecognized type"
+
+-- | Optional rewrites to do when resolving a term
+data ResolveRewrite = ResolveRewrite {
+  rrBasicSS :: Maybe (Simpset TheoremNonce),
+  -- ^ Rewrite terms using these rewrites
+
+  rrWhat4Eval :: Bool
+  -- ^ Also simplify terms using What4 evaluation
+}
+
+-- | Don't do any rewriting
+noResolveRewrite :: ResolveRewrite
+noResolveRewrite = ResolveRewrite { rrBasicSS = Nothing, rrWhat4Eval = False }
+
+-- Convert a term to a What4 expression, trying to simplify it in the process.
+-- Currently this expects the terms to be either boolean or bit-vectors, as
+-- that's all we use it for.   It should be fairly straightforward to generalize
+-- if need be.
+resolveTerm ::
+  Sym {- ^ Backend state -} ->
+  Set VarIndex {- ^ Keep these opaque -} ->
+  W4.BaseTypeRepr t  {- ^ Type of term -} ->
+  ResolveRewrite {- ^ Optional rewrites to do on the term -} ->
+  Term {- ^ Term to process -} ->
+  IO (Crucible.RegValue Sym (Crucible.BaseToType t))
+resolveTerm sym unint bt rr tm =
+  do
+    st       <- sawCoreState sym
+    checkType st
+    tm'      <- basicRewrite st tm
+    case () of
+      _ | isConstFoldTerm unint tm' ->
+          do -- Evaluate as constant
+            modmap <- scGetModuleMap (saw_ctx st)
+            let v = Concrete.evalSharedTerm modmap mempty mempty tm'
+            case bt of
+              W4.BaseBoolRepr -> pure (W4.backendPred sym (Concrete.toBool v))
+              W4.BaseBVRepr w -> W4.bvLit sym w (BV.mkBV w (Prim.unsigned (Concrete.toWord v)))
+              _ -> fail "resolveTerm: expected `Bool` or bit-vector"
+
+        | rrWhat4Eval rr ->
+          do -- Try to use rewrites to simplify the term
+            let sc = saw_ctx st
+            cryptol_ss <- Cryptol.mkCryptolSimpset @TheoremNonce sc
+            tm''       <- snd <$> rewriteSharedTerm sc cryptol_ss tm'
+            tm'''      <- basicRewrite st tm''
+            if all isPreludeName (Map.elems (getConstantSet tm''')) then
+              do
+                (_, _, _, p) <- w4EvalAny sym st sc mempty unint tm'''
+                case valueToSymExpr p of
+                  Just (Some y)
+                    | Just Refl <- testEquality bt ty -> pure y
+                    | otherwise -> typeError (show ty)
+                    where ty = W4.exprType y
+                  _ -> fail ("resolveTerm: unexpected w4Eval result " ++ show p)
+              else
+                bindSAWTerm sym st bt tm'''
+
+          -- Just bind the term
+        | otherwise -> bindSAWTerm sym st bt tm'
+
+  where
+  basicRewrite st =
+    case rrBasicSS rr of
+      Nothing -> pure
+      Just ss -> \t -> snd <$> rewriteSharedTerm (saw_ctx st) ss t
+
+  isPreludeName nm =
+    case nm of
+      ModuleIdentifier ident -> identModule ident == preludeName
+      _ -> False
+
+  checkType st =
+    do
+      sc <- ttType <$> mkTypedTerm (saw_ctx st) tm
+      case ttIsMono sc of
+          Just ty
+            | tIsBit ty, W4.BaseBoolRepr <- bt -> pure ()
+            | Just (n,el) <- (tIsSeq ty)
+            , tIsBit el, Just i <- tIsNum n, W4.BaseBVRepr w <- bt
+            , intValue w == i -> pure ()
+            | otherwise -> typeError (show (PP.pp ty)) :: IO ()
+          Nothing -> typeError (show (ppTypedTermType sc))
+
+  typeError :: String -> IO a
+  typeError t = fail $ unlines [
+    "Expected type: " ++ (
+      case bt of
+        W4.BaseBoolRepr  -> "Bit"
+        W4.BaseBVRepr w  -> "[" ++ show w ++ "]"
+        _             -> show bt),
+    "Actual type:   " ++ t
+    ]
+
+-- 'resolveTerm' specialized to booleans.
+resolveBoolTerm' :: Sym -> Set VarIndex -> ResolveRewrite -> Term -> IO (W4.Pred Sym)
+resolveBoolTerm' sym unint = resolveTerm sym unint W4.BaseBoolRepr
+
+-- 'resolveTerm' specialized to booleans, without rewriting.
+resolveBoolTerm :: Sym -> Set VarIndex -> Term -> IO (W4.Pred Sym)
+resolveBoolTerm sym unint = resolveBoolTerm' sym unint noResolveRewrite
+
+-- 'resolveTerm' specialized to bit-vectors.
+resolveBitvectorTerm' ::
+  (1 W4.<= w) => Sym -> Set VarIndex -> W4.NatRepr w -> ResolveRewrite -> Term -> IO (W4.SymBV Sym w)
+resolveBitvectorTerm' sym unint w = resolveTerm sym unint (W4.BaseBVRepr w)
+
+-- 'resolveTerm' specialized to bit-vectors, without rewriting.
+resolveBitvectorTerm :: 
+  (1 W4.<= w) => Sym -> Set VarIndex -> W4.NatRepr w -> Term -> IO (W4.SymBV Sym w)
+resolveBitvectorTerm sym unint w = resolveBitvectorTerm' sym unint w noResolveRewrite
+

saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs

@@ -8,35 +8,59 @@ Stability   : provisional
 
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE ParallelListComp #-}
+{-# LANGUAGE RankNTypes #-}
 
 module SAWCentral.Crucible.Common.Setup.Builtins
   ( crucible_precond
   , crucible_postcond
   , crucible_return
   , crucible_execute_func
   , crucible_equal
+  , declare_unint
   , CheckPointsToType(..)
   ) where
 
 import           Control.Lens
 import           Control.Monad (when)
 import           Control.Monad.State (get)
 import qualified Data.Map as Map
+import           Data.Set(Set)
+import qualified Data.Set as Set
+import           Data.Text(Text)
 
 import qualified What4.ProgramLoc as W4
 
+import           SAWCore.Name(VarIndex)
 import           CryptolSAWCore.TypedTerm (TypedTerm)
 
 import           SAWCentral.Value
 
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import           SAWCentral.Crucible.Common.Setup.Type
+import           SAWCentral.Builtins(resolveNames)
 
 --------------------------------------------------------------------------------
 -- ** Builtins
 
 -- TODO: crucible_fresh_var?
 
+-- | Declare a particular name as opaque
+declare_unint ::
+  String {- ^ Name of command for error messages -} ->
+  Setter' (MS.CrucibleContext ext) (Set VarIndex) {-^ Keep uninterpreted names here -} ->
+  [Text] {- ^ Names for the things to be left uninterpreted -} ->
+  CrucibleSetup ext ()
+declare_unint cmd unintF names = 
+  do
+    prePost <- use csPrePost
+    case prePost of
+      MS.PreState ->
+        do
+          ns <- crucibleSetupTopLevel (resolveNames names)
+          csCrucibleContext . unintF %= Set.union ns
+      MS.PostState ->
+        fail ("`" ++ cmd ++ "` works only in the pre-condition of a specification.")
+
 crucible_precond ::
   W4.ProgramLoc ->
   TypedTerm ->

saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs

@@ -46,6 +46,7 @@ module SAWCentral.Crucible.JVM.Builtins
     , jvm_setup_with_tag
     , jvm_ghost_value
     , jvm_equal
+    , jvm_unint
     ) where
 
 import           Control.Lens
@@ -139,6 +140,7 @@ import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import qualified SAWCentral.Crucible.Common.Setup.Type as Setup
 import qualified SAWCentral.Crucible.Common.Setup.Builtins as Setup
+import SAWCentral.Crucible.JVM.Setup.Value(jccUninterp)
 import SAWCentral.Crucible.JVM.MethodSpecIR
 import SAWCentral.Crucible.JVM.Override
 import SAWCentral.Crucible.JVM.ResolveSetupValue
@@ -862,6 +864,7 @@ setupCrucibleContext jclass =
                                , _jccBackend = bak
                                , _jccJVMContext = jc
                                , _jccHandleAllocator = halloc
+                               , _jccUninterp = mempty
                                }
 
 --------------------------------------------------------------------------------
@@ -1474,6 +1477,9 @@ jvm_equal val1 val2 =
        ]
      Setup.crucible_equal loc val1 val2
 
+jvm_unint :: [Text] -> JVMSetupM ()
+jvm_unint term = JVMSetupM (Setup.declare_unint "jvm_unint" jccUninterp term)
+
 --------------------------------------------------------------------------------
 
 -- | Sort a list of things and group them into equivalence classes.