From 86ef62645d9d8f742e925c567ad26ea9d1e77c11 Mon Sep 17 00:00:00 2001
From: Nathan Collins <conathan@galois.com>
Date: Thu, 17 Jan 2019 14:25:59 -0800
Subject: [PATCH 1/3] Fill in `undefined`s with nonsense so pretty printing
 works

---
 symbolic/src/Data/Macaw/Symbolic/CrucGen.hs | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
index b74b7a61..0e1276de 100644
--- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+++ b/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

From f2b98011ce62c2cb27addb6f6a25a17fac6be43a Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 21 Jan 2019 11:40:45 -0800
Subject: [PATCH 2/3] Use initSimContext to create a Crucible SimContext.

This helps to immunize against changes in SimContext... e.g. the
addition on the profilingMetrics field that initSimContext provides a
default value for.
---
 symbolic/src/Data/Macaw/Symbolic.hs | 17 ++++++-----------
 1 file changed, 6 insertions(+), 11 deletions(-)

diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs
index 61033894..aaae7fe3 100644
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/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 $

From 7eabf2d01a45d1723a8acfe53398582957ed6d38 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 21 Jan 2019 12:20:48 -0800
Subject: [PATCH 3/3] Handle additional side conditions returned by
 loadRawWithSideConditions.

---
 symbolic/src/Data/Macaw/Symbolic/MemOps.hs | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs b/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
index 4f399b99..c9d23570 100644
--- a/symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+++ b/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