From b66de78b7eaa6c95b25817501b937cd7d0221562 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Fri, 8 Jul 2022 09:33:57 -0700
Subject: [PATCH] Add specification preconditions to the assumption state prior
 to beginning symbolic execution instead of just before asserting
 postconditions.

This allows the assumptions to be in scope for safety conditions
that arise durning execution.
---
 src/SAWScript/Crucible/LLVM/Builtins.hs |  1 +
 src/SAWScript/Crucible/LLVM/X86.hs      | 20 +++++++++++++-------
 2 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 909f6ef01d..a2042501b3 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -80,6 +80,7 @@ module SAWScript.Crucible.LLVM.Builtins
     , findDecl
     , findDefMaybeStatic
     , setupLLVMCrucibleContext
+    , setupPrestateConditions
     , checkSpecReturnType
     , verifyPrestate
     , verifyPoststate
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index 568c85759c..81518c9dde 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -474,12 +474,24 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
               , C._cruciblePersonality = Macaw.MacawSimulatorState
               , C._profilingMetrics = Map.empty
               }
-        globals = C.insertGlobal mvar (preState ^. x86Mem) C.emptyGlobals
+
+      (globals, assumes) <-
+          do let globals0 = C.insertGlobal mvar (preState ^. x86Mem) C.emptyGlobals
+             liftIO $ setupPrestateConditions methodSpec cc (preState ^. x86Mem) env globals0
+                       (methodSpec ^. MS.csPreState . MS.csConditions)
+
+      let
         macawStructRepr = C.StructRepr $ Macaw.crucArchRegTypes Macaw.x86_64MacawSymbolicFns
         initial = C.InitialState ctx globals C.defaultAbortHandler macawStructRepr
                   $ C.runOverrideSim macawStructRepr
                   $ Macaw.crucGenArchConstraints Macaw.x86_64MacawSymbolicFns
                   $ do
+          liftIO $
+            forM_ assumes $ \(C.LabeledPred p (md, reason)) ->
+              do expr <- resolveSAWPred cc p
+                 let loc = MS.conditionLoc md
+                 C.addAssumption bak
+                   (C.GenericAssumption loc reason expr)
           r <- C.callCFG cfg . C.RegMap . singleton . C.RegEntry macawStructRepr $ preState ^. x86Regs
           globals' <- C.readGlobals
           mem' <- C.readGlobal mvar
@@ -1083,9 +1095,6 @@ assertPost globals env premem preregs mdMap = do
   pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos)
     $ assertPointsTo env tyenv nameEnv
 
-  let setupConditionMatchesPre = fmap -- assume preconditions
-        (LO.executeSetupCondition opts sc cc ms)
-        $ ms ^. MS.csPreState . MS.csConditions
   let setupConditionMatchesPost = fmap -- assert postconditions
         (LO.learnSetupCondition opts sc cc ms MS.PostState)
         $ ms ^. MS.csPostState . MS.csConditions
@@ -1105,15 +1114,12 @@ assertPost globals env premem preregs mdMap = do
     . sequence_ $ mconcat
     [ returnMatches
     , pointsToMatches
-    , setupConditionMatchesPre
     , setupConditionMatchesPost
     , [LO.assertTermEqualities sc cc]
     ]
   st <- case result of
     Left err -> throwX86 $ show err
     Right (_, st) -> pure st
-  liftIO . forM_ (view O.osAssumes st) $ \(_md, asum) ->
-    C.addAssumption bak $ C.GenericAssumption (st ^. O.osLocation) "precondition" asum
   liftIO . forM_ (view LO.osAsserts st) $ \(md, W4.LabeledPred p r) ->
        do (ann,p') <- W4.annotateTerm sym p
           modifyIORef mdMap (Map.insert ann md)