Merge pull request #847 from GaloisInc/x86-return-trunc

x86: Truncate RAX when matching smaller return values

intTests/test_llvm_x86_05/test.S

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

intTests/test_llvm_x86_05/test.c

@@ -0,0 +1,8 @@
+#include <stdint.h>
+#include <stdio.h>
+
+extern uint32_t returntest();
+
+uint32_t test() {
+	return returntest();
+};

intTests/test_llvm_x86_05/test.saw

@@ -0,0 +1,10 @@
+enable_experimental;
+
+m <- llvm_load_module "test.bc";
+
+let returntest_setup = do {
+  crucible_execute_func [];
+
+  crucible_return (crucible_term {{ 42 : [32] }});
+};
+crucible_llvm_verify_x86 m "./test" "returntest" [] false returntest_setup w4;

intTests/test_llvm_x86_05/test.sh

@@ -0,0 +1,6 @@
+set -e
+
+yasm -felf64 test.S
+ld test.o -o test
+clang -c -emit-llvm test.c
+$SAW test.saw

src/SAWScript/Crucible/LLVM/X86.hs

@@ -722,7 +722,22 @@ assertPost globals env premem preregs = do
   returnMatches <- case (ms ^. MS.csRetValue, ms ^. MS.csRet) of
     (Just expectedRet, Just retTy) -> do
       postRAX <- C.LLVM.ptrToPtrVal <$> getReg Macaw.RAX postregs
-      pure [LO.matchArg opts sc cc ms MS.PostState postRAX retTy expectedRet]
+      case (postRAX, C.LLVM.memTypeBitwidth retTy) of
+        (C.LLVM.LLVMValInt base off, Just retTyBits) -> do
+          let
+            truncateRAX :: forall r. NatRepr r -> X86Sim (C.LLVM.LLVMVal Sym)
+            truncateRAX rsz =
+              case (testLeq (knownNat @1) rsz, testLeq rsz (W4.bvWidth off)) of
+                (Just LeqProof, Just LeqProof) ->
+                  case testStrictLeq rsz (W4.bvWidth off) of
+                    Left LeqProof -> do
+                      offTrunc <- liftIO $ W4.bvTrunc sym rsz off
+                      pure $ C.LLVM.LLVMValInt base offTrunc
+                    _ -> pure $ C.LLVM.LLVMValInt base off
+                _ -> throwX86 "Width of return type is zero bits"
+          postRAXTrunc <- viewSome truncateRAX (mkNatRepr retTyBits)
+          pure [LO.matchArg opts sc cc ms MS.PostState postRAXTrunc retTy expectedRet]
+        _ -> throwX86 $ "Invalid return type: " <> show (C.LLVM.ppMemType retTy)
     _ -> pure []
 
   pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos)