x86: Properly include assumed preconditions in goals (#1095)

* x86: Properly assume preconditions

* x86: Add an integration test

Author: chameco

intTests/test_llvm_x86_07/test

@@ -0,0 +1,10 @@
+section .bss
+section .text
+global precondtest
+precondtest:
+	mov rax, rdi
+        ret
+global _start
+_start:
+        mov rax, 60
+        syscall

intTests/test_llvm_x86_07/test.S

@@ -0,0 +1,8 @@
+#include <stdint.h>
+#include <stdio.h>
+
+extern uint64_t precondtest(uint64_t x);
+
+void test() {
+	precondtest(1);
+};

intTests/test_llvm_x86_07/test.c

@@ -0,0 +1,14 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+let precondtest_setup = do {
+  x <- crucible_fresh_var "x" (llvm_int 64);
+  crucible_precond {{ x < 10 }};
+  llvm_execute_func [crucible_term x];
+  x' <- crucible_fresh_var "x'" (llvm_int 64);
+  crucible_return (crucible_term x');
+  crucible_postcond {{ x' < 10 }};
+};
+
+llvm_verify_x86 m "./test" "precondtest" [] false precondtest_setup w4;

intTests/test_llvm_x86_07/test.saw

@@ -0,0 +1,7 @@
+#!/bin/sh
+set -e
+
+# yasm -felf64 test.S
+# ld test.o -o test
+clang -c -emit-llvm test.c
+$SAW test.saw

intTests/test_llvm_x86_07/test.sh

@@ -38,6 +38,7 @@ module SAWScript.Crucible.LLVM.Override
 
   , learnCond
   , learnSetupCondition
+  , executeSetupCondition
   , matchArg
   , assertTermEqualities
   , methodSpecHandler

src/SAWScript/Crucible/LLVM/Override.hs

@@ -72,6 +72,7 @@ import SAWScript.X86 hiding (Options)
 import SAWScript.X86Spec
 import SAWScript.Crucible.Common
 
+import qualified SAWScript.Crucible.Common as Common
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
 import qualified SAWScript.Crucible.Common.Override as O
 import qualified SAWScript.Crucible.Common.Setup.Type as Setup
@@ -437,7 +438,15 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
 
       liftIO $ C.executeCrucible execFeatures initial >>= \case
         C.FinishedResult{} -> pure ()
-        C.AbortedResult{} -> printOutLn opts Warn "Warning: function never returns"
+        C.AbortedResult _ ar -> do
+          printOutLn opts Warn "Warning: function never returns"
+          print $ Common.ppAbortedResult
+            ( \gp ->
+                case C.lookupGlobal mvar $ gp ^. C.gpGlobals of
+                  Nothing -> "LLVM memory global variable not initialized"
+                  Just mem -> C.LLVM.ppMem $ C.LLVM.memImplHeap mem
+            )
+            ar
         C.TimeoutResult{} -> fail "Execution timed out"
 
       stats <- checkGoals sym opts sc tactic
@@ -870,7 +879,10 @@ assertPost globals env premem preregs = do
   pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos)
     $ assertPointsTo env tyenv nameEnv
 
-  let setupConditionMatches = fmap
+  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
 
@@ -889,12 +901,15 @@ assertPost globals env premem preregs = do
     . sequence_ $ mconcat
     [ returnMatches
     , pointsToMatches
-    , setupConditionMatches
+    , 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) $ \p ->
+    C.addAssumption sym . C.LabeledPred p $ C.AssumptionReason (st ^. O.osLocation) "precondition"
   liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) ->
     C.addAssertion sym $ C.LabeledPred p r