Implement llvm_assert and jvm_assert.

Fixes #1644
GaloisInc · May 20, 2022 · bf5dd74 · bf5dd74
1 parent 31fa250
commit bf5dd74
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 0 deletions.
diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -31,6 +31,7 @@ module SAWScript.Crucible.JVM.Builtins
     , jvm_execute_func
     , jvm_postcond
     , jvm_precond
+    , jvm_assert
     , jvm_modifies_field
     , jvm_modifies_static_field
     , jvm_modifies_elem
@@ -1255,6 +1256,11 @@ generic_array_is ptr mval =
        X.throwM $ JVMArrayModifyPrestate ptr'
      Setup.addPointsTo pt
 
+jvm_assert :: TypedTerm -> JVMSetupM ()
+jvm_assert term = JVMSetupM $ do
+  loc <- SS.toW4Loc "jvm_assert" <$> lift getPosition
+  Setup.addCondition (MS.SetupCond_Pred loc term)
+
 jvm_precond :: TypedTerm -> JVMSetupM ()
 jvm_precond term = JVMSetupM $ do
   loc <- SS.toW4Loc "jvm_precond" <$> lift getPosition

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -30,6 +30,7 @@ module SAWScript.Crucible.LLVM.Builtins
     , llvm_return
     , llvm_precond
     , llvm_postcond
+    , llvm_assert
     , llvm_cfg
     , llvm_extract
     , llvm_compositional_extract
@@ -1732,6 +1733,12 @@ checkMemTypeCompatibility loc t1 t2 =
 --------------------------------------------------------------------------------
 -- Setup builtins
 
+llvm_assert :: TypedTerm -> LLVMCrucibleSetupM ()
+llvm_assert term =
+  LLVMCrucibleSetupM $
+  do loc <- getW4Position "llvm_assert"
+     Setup.addCondition (MS.SetupCond_Pred loc term)
+
 llvm_precond :: TypedTerm -> LLVMCrucibleSetupM ()
 llvm_precond term =
   LLVMCrucibleSetupM $

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
@@ -2639,6 +2639,14 @@ primitives = Map.fromList
     Current
     [ "Legacy alternative name for `llvm_precond`." ]
 
+  , prim "llvm_assert" "Term -> LLVMSetup ()"
+    (pureVal llvm_assert)
+    Current
+    [ "State that the given predicate must hold.  Acts as `llvm_precond`"
+    , "or `llvm_postcond` depending on the phase of specification in which"
+    , "it appears (i.e., before or after `llvm_execute_func`."
+    ]
+
   , prim "llvm_postcond" "Term -> LLVMSetup ()"
     (pureVal llvm_postcond)
     Current
@@ -3145,6 +3153,14 @@ primitives = Map.fromList
     , "method being verified."
     ]
 
+  , prim "jvm_assert" "Term -> JVMSetup ()"
+    (pureVal jvm_assert)
+    Current
+    [ "State that the given predicate must hold.  Acts as `jvm_precond`"
+    , "or `jvm_postcond` depending on the phase of specification in which"
+    , "it appears (i.e., before or after `jvm_execute_func`."
+    ]
+
   , prim "jvm_postcond" "Term -> JVMSetup ()"
     (pureVal jvm_postcond)
     Current