Update llvm-pretty and llvm-pretty-bc-parser submodules (#333)

* Update llvm-pretty and llvm-pretty-bc-parser submodules * Update crucible submodule to track llvm-pretty* changes * Changes for updated Crucible submodule - TimeoutResult from symbolic simulator - New X86_FP80 type * Update llvm-verifier submodule to account for llvm-pretty* changes
GaloisInc · Dec 15, 2018 · bbbb4ad · bbbb4ad
1 parent 217893c
commit bbbb4ad
Show file tree

Hide file tree

Showing 8 changed files with 25 additions and 13 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/llvm-pretty b/deps/llvm-pretty
diff --git a/deps/llvm-pretty-bc-parser b/deps/llvm-pretty-bc-parser
diff --git a/deps/llvm-verifier b/deps/llvm-verifier
diff --git a/saw-script.cabal b/saw-script.cabal
@@ -48,7 +48,7 @@ library
     , jvm-parser
     , jvm-verifier
     , lens
-    , llvm-pretty >= 0.5
+    , llvm-pretty >= 0.8
     , llvm-pretty-bc-parser >= 0.1.3.1
     , llvm-verifier >= 0.2.1
     , monad-supply

diff --git a/src/SAWScript/CrucibleBuiltins.hs b/src/SAWScript/CrucibleBuiltins.hs
@@ -173,8 +173,13 @@ crucible_llvm_verify bic opts lm nm lemmas checkSat setup tactic =
      setupLoc <- toW4Loc "_SAW_verify_prestate" <$> getPosition
 
      def <- case find (\d -> L.defName d == nm') (L.modDefines llmod) of
-                    Nothing -> fail ("Could not find function named" ++ show nm)
-                    Just decl -> return decl
+              Just decl -> return decl
+              Nothing   -> fail $ unlines $
+                [ "Could not find function named " ++ show nm
+                ] ++ if simVerbose opts < 3
+                     then [ "Run SAW with --sim-verbose=3 to see all function names" ]
+                     else "Available function names:" :
+                            map (("  " ++) . show . L.defName) (L.modDefines llmod)
      st0 <- either (fail . show . ppSetupError) return (initialCrucibleSetupState cc def setupLoc)
 
      -- execute commands of the method spec
@@ -185,7 +190,7 @@ crucible_llvm_verify bic opts lm nm lemmas checkSat setup tactic =
      let globals = cc^.ccLLVMGlobals
      let mvar = Crucible.llvmMemVar (cc^.ccLLVMContext)
      mem0 <- case Crucible.lookupGlobal mvar globals of
-       Nothing -> fail "internal error: LLVM Memory global not found"
+       Nothing   -> fail "internal error: LLVM Memory global not found"
        Just mem0 -> return mem0
      let globals1 = Crucible.llvmGlobals (cc^.ccLLVMContext) mem0
 
@@ -1038,10 +1043,13 @@ constructExpandedSetupValue sc loc t =
     Crucible.ArrayType n memTy ->
        SetupArray <$> replicateM n (constructExpandedSetupValue sc loc memTy)
 
-    Crucible.FloatType    -> fail "crucible_fresh_expanded_var: Float not supported"
-    Crucible.DoubleType   -> fail "crucible_fresh_expanded_var: Double not supported"
-    Crucible.MetadataType -> fail "crucible_fresh_expanded_var: Metadata not supported"
-    Crucible.VecType{}    -> fail "crucible_fresh_expanded_var: Vec not supported"
+    Crucible.FloatType      -> failUnsupportedType "Float"
+    Crucible.DoubleType     -> failUnsupportedType "Double"
+    Crucible.MetadataType   -> failUnsupportedType "Metadata"
+    Crucible.VecType{}      -> failUnsupportedType "Vec"
+    Crucible.X86_FP80Type{} -> failUnsupportedType "X86_FP80"
+  where failUnsupportedType tyName = fail $ unwords
+          ["crucible_fresh_expanded_var: " ++ tyName ++ " not supported"]
 
 llvmTypeAlias :: L.Type -> Maybe Crucible.Ident
 llvmTypeAlias (L.Alias i) = Just i

diff --git a/src/SAWScript/CrucibleBuiltinsJVM.hs b/src/SAWScript/CrucibleBuiltinsJVM.hs
@@ -162,7 +162,7 @@ crucible_java_extract bic opts c mname = do
 
           res <- CJ.runMethodHandle sym CrucibleSAW.SAWCruciblePersonality halloc
                      ctx verbosity className h args
-                         
+
           case res of
             Crucible.FinishedResult _ pr -> do
               gp <- getGlobalPair opts pr
@@ -175,3 +175,5 @@ crucible_java_extract bic opts c mname = do
               mkTypedTerm sc t'
             Crucible.AbortedResult _ _ar -> do
               fail $ unlines [ "Symbolic execution failed." ]
+            Crucible.TimeoutResult _cxt -> do
+              fail $ unlines [ "Symbolic execution timed out." ]
diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
@@ -518,6 +518,8 @@ doSim opts elf sfs name (globs,overs) st =
                    malformed $ unlines [ "Failed to finish execution"
                                        , ppAbort mvar res
                                        ]
+             TimeoutResult _ctx ->
+                   malformed $ unlines [ "Execution timed out" ]
 
      mem <- getMem gp mvar
      return ( addrInt
+1 −1		crucible-c/src/CrucibleCMain.hs
+2 −2		crucible-llvm/crucible-llvm.cabal
+10 −3		crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs
+45 −0		crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs
+10 −1		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+144 −57		crucible-saw/src/Lang/Crucible/Backend/SAWCore.hs
+16 −23		crucible-syntax/crucible-syntax/Main.hs
+0 −1		crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs
+0 −1		crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+1 −3		crucible-syntax/src/Lang/Crucible/Syntax/SExpr.hs
+1 −1		crucible-syntax/test-data/simulator-tests/override-test2.out.good
+1 −1		crucible/src/Lang/Crucible/Simulator/BoundedExec.hs
+5 −5		crux/src/Crux/Options.hs
+1 −1		dependencies/llvm-pretty
+1 −1		dependencies/llvm-pretty-bc-parser
+47 −3		what4/src/What4/Protocol/SMTLib2/Syntax.hs
+2 −1		what4/test/ExprBuilderSMTLib2.hs
+36 −5		README.md
+4 −1		disasm-test/cpp/README.md
+12 −0		disasm-test/cpp/atomicrmw.cpp
+26,411 −0		disasm-test/cpp/atomicrmw.ll
+17 −0		disasm-test/cpp/atomicrmw.nix
+12 −0		disasm-test/cpp/libcxxbc.nix
+15 −0		fuzzing/README.md
+18 −17		llvm-disasm/LLVMDis.hs
+7 −6		llvm-pretty-bc-parser.cabal
+62 −0		src/Data/LLVM/BitCode/Assert.hs
+19 −21		src/Data/LLVM/BitCode/IR/Constants.hs
+136 −33		src/Data/LLVM/BitCode/IR/Function.hs
+29 −23		src/Data/LLVM/BitCode/IR/Metadata.hs
+4 −22		src/Data/LLVM/BitCode/IR/Module.hs
+11 −10		src/Data/LLVM/BitCode/IR/Types.hs
+17 −12		src/Data/LLVM/BitCode/Parse.hs
+6 −6		llvm-verifier.cabal
+3 −1		src/Verifier/LLVM/Codebase/Translation.hs