Merge branch 'master' into refinement

symbolic/src/Data/Macaw/Symbolic.hs

@@ -658,17 +658,12 @@ runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH g regStruct = d
   let macawStructRepr = C.StructRepr crucRegTypes
 
   let ctx :: C.SimContext (MacawSimulatorState sym) sym (MacawExt arch)
-      ctx = C.SimContext { C._ctxSymInterface = sym
-                         , C.ctxSolverProof = \a -> a
-                         , C.ctxIntrinsicTypes = llvmIntrinsicTypes
-                         , C.simHandleAllocator = halloc
-                         , C.printHandle = stdout
-                         , C.extensionImpl = macawExtensions archEval mvar globs lookupH
-                         , C._functionBindings =
-                              C.insertHandleMap (C.cfgHandle g) (C.UseCFG g (C.postdomInfo g)) $
-                              C.emptyHandleMap
-                         , C._cruciblePersonality = MacawSimulatorState
-                         }
+      ctx = let fnBindings = C.insertHandleMap (C.cfgHandle g)
+                             (C.UseCFG g (C.postdomInfo g)) $
+                             C.emptyHandleMap
+                extImpl = macawExtensions archEval mvar globs lookupH
+            in C.initSimContext sym llvmIntrinsicTypes halloc stdout
+               fnBindings extImpl MacawSimulatorState
   -- Create the symbolic simulator state
   let initGlobals = C.insertGlobal mvar initMem C.emptyGlobals
   let s = C.InitialState ctx initGlobals C.defaultAbortHandler $

symbolic/src/Data/Macaw/Symbolic/CrucGen.hs

@@ -1266,10 +1266,14 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
       addTermStmt $ CR.Jump (parsedBlockLabel blockLabelMap nextAddr 0)
     M.ParsedLookupTable regs _idx _possibleAddrs -> do
       setMachineRegs =<< createRegStruct regs
-      let cond = undefined
+      -- WARNING: the 'cond', 'tlbl', and 'flbl' values here are all
+      -- nonsense. They were 'undefined', but that makes pretty
+      -- printing crash so we use defined but nonsensical values
+      -- instead.
+      cond <- crucibleValue (C.BoolLit True)
       -- TODO: Add ability in CrucGen to generate new labels and add new blocks.
-      let tlbl = undefined
-      let flbl = undefined
+      let tlbl = parsedBlockLabel blockLabelMap thisAddr 0
+      let flbl = tlbl
       addTermStmt $! CR.Br cond tlbl flbl
     M.ParsedReturn regs -> do
       regValues <- createRegStruct regs

symbolic/src/Data/Macaw/Symbolic/MemOps.hs

@@ -476,14 +476,18 @@ doCondReadMem st mvar globs w (BVMemRepr bytes endian) cond0 ptr0 def0 =
 
      let useDefault msg =
            do notC <- notPred sym cond
-              assert sym notC
-                 (AssertFailureSimError ("[doCondReadMem] " ++ msg))
+              assert sym notC $ failWithMsg msg
               return def
+         failWithMsg msg = AssertFailureSimError ("[doCondReadMem] " ++ msg)
 
      a <- case val of
-            Right (p,r,v) | Just a <- valToBits bitw v ->
-              do grd <- impliesPred sym cond p
-                 assert sym grd r
+            Right (v,p1,p2,p3) | Just a <- valToBits bitw v ->
+              do grd1 <- impliesPred sym cond p1
+                 assert sym grd1 $ failWithMsg "memory region is allocated"
+                 grd2 <- impliesPred sym cond p2
+                 assert sym grd2 $ failWithMsg "memory region is properly aligned"
+                 grd3 <- impliesPred sym cond p3
+                 assert sym grd3 $ failWithMsg "memory region validated (see MemModel.Generic)"
                  muxLLVMPtr sym cond a def
             Right _ -> useDefault "Unexpected value read from memory."
             Left err -> useDefault err