From bf5dd741c9161c3c1d8af73218ac9a9cbf229992 Mon Sep 17 00:00:00 2001
From: Robert Dockins <rdockins@galois.com>
Date: Thu, 19 May 2022 14:01:25 -0700
Subject: [PATCH] Implement `llvm_assert` and `jvm_assert`.

Fixes #1644
---
 src/SAWScript/Crucible/JVM/Builtins.hs  |  6 ++++++
 src/SAWScript/Crucible/LLVM/Builtins.hs |  7 +++++++
 src/SAWScript/Interpreter.hs            | 16 ++++++++++++++++
 3 files changed, 29 insertions(+)

diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index 1e24eeaf13..b71123f344 100644
--- 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
index 38216bf027..f8eabbff75 100644
--- 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
index 474355b76e..14606c455d 100644
--- 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