Merge pull request #154 from GaloisInc/feature/normflat2

Update macaw-aarch32 for changes to the ASL translator

.travis.yml

@@ -19,6 +19,7 @@ install:
 # our submodules without worrying about ssh keys.
 - sed -i 's/git@github.com:/https:\/\/github.com\//' .gitmodules
 - git submodule update --init
+- cabal v2-configure --project-file=cabal.project.dist --flags="+asl-lite"
 - cabal v2-update --project-file=cabal.project.dist
 
 script:
@@ -26,3 +27,4 @@ script:
 # any command which exits with a non-zero exit code causes the build to fail.
  # Build packages
  - cabal v2-test --project-file=cabal.project.dist x86 x86_symbolic
+ - cabal v2-test --project-file=cabal.project.dist macaw-asl-tests

deps/asl-translator

@@ -1 +1 @@
-Subproject commit 808f2d2ea51ec0c8fd60a32a5d9b944274e166b9
+Subproject commit d0bac677e038a54f47af0467e68c4aab95a32d64

deps/crucible

@@ -1 +1 @@
-Subproject commit f4d6f6bb5b30050c0089bed17e0f98132db433eb
+Subproject commit 5cb47b4f77299b54b0ead3f93f25dc24447c80f3

deps/dismantle

@@ -1 +1 @@
-Subproject commit 21c5d44d2fdfe5bfbed6278668ddd433668218a9
+Subproject commit 1f61d7259228bbfb51053e7c990fac6d9228e154

deps/flexdis86

@@ -1 +1 @@
-Subproject commit 5981054db6354e0deb54323d93274d66e6a119f9
+Subproject commit 51317819dbb7a39891f36010d3c4bf196789d032

deps/semmc

@@ -1 +1 @@
-Subproject commit 120eef4f1900f70adb5a306014c2cc2f3c17b4c5
+Subproject commit 990ce7ab63dd67cf0f23876d5d4d93da507ec11e

deps/what4

@@ -1 +1 @@
-Subproject commit a1290af1d571b2bcbc42ebe0ae455f2a3b184874
+Subproject commit f9a8f950e7c66f0f04312ce3983a42f3facd576e

deps/what4-serialize

@@ -1 +1 @@
-Subproject commit 140ad099d7856c35d03ee8f18a94af00867b8eff
+Subproject commit e0a013a24a459a71f96a2238a238ff4f3bc9f111

macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs

@@ -32,6 +32,7 @@ import           Data.Parameterized.Some ( Some(..) )
 import qualified Data.Parameterized.SymbolRepr as PSR
 import qualified Data.Parameterized.TraversableFC as FC
 import qualified Data.Parameterized.TH.GADT as PTH
+import qualified Data.Parameterized.List as P
 import qualified Data.Set as Set
 import qualified Data.Text as T
 import           GHC.TypeLits
@@ -73,7 +74,7 @@ data ARMReg tp where
                    , tp' ~ ASL.GlobalsType s
                    , tp ~ BaseToMacawType tp')
                 => ASL.GlobalRef s -> ARMReg tp
-  ARMWriteMode :: tp ~ MT.BVType 2 => ARMReg (MT.BVType 2)
+  ARMDummyReg :: ARMReg (MT.TupleType '[])
 
 -- | GPR14 is the link register for ARM
 arm_LR :: (w ~ MC.RegAddrWidth ARMReg, 1 <= w) => ARMReg (MT.BVType w)
@@ -86,7 +87,7 @@ instance Show (ARMReg tp) where
   show r = case r of
     ARMGlobalBV globalRef -> show (ASL.globalRefSymbol globalRef)
     ARMGlobalBool globalRef -> show (ASL.globalRefSymbol globalRef)
-    ARMWriteMode -> "ARMWriteMode"
+    ARMDummyReg -> "()"
 
 instance ShowF ARMReg where
     showF = show
@@ -125,7 +126,7 @@ instance MT.HasRepr ARMReg MT.TypeRepr where
         case r of
           ARMGlobalBV globalRef -> baseToMacawTypeRepr (ASL.globalRefRepr globalRef)
           ARMGlobalBool globalRef -> baseToMacawTypeRepr (ASL.globalRefRepr globalRef)
-          ARMWriteMode -> MT.BVTypeRepr (NR.knownNat @2)
+          ARMDummyReg -> MT.TupleTypeRepr P.Nil
 
 type instance MC.ArchReg SA.AArch32 = ARMReg
 type instance MC.RegAddrWidth ARMReg = 32
@@ -151,6 +152,7 @@ armRegs = FC.toListFC asARMReg ( FC.fmapFC ASL.SimpleGlobalRef ASL.simpleGlobalR
         asARMReg gr = case ASL.globalRefRepr gr of
           WT.BaseBoolRepr -> Some (ARMGlobalBool gr)
           WT.BaseBVRepr _ -> Some (ARMGlobalBV gr)
+          WT.BaseStructRepr Ctx.Empty -> Some ARMDummyReg
           tp -> error $ "unsupported global type " <> show tp
 
 -- | The set of registers preserved across Linux system calls is defined by the ABI.
@@ -185,6 +187,8 @@ locToRegTH (SA.Location globalRef) = do
       [| ARMGlobalBool (ASL.knownGlobalRef :: ASL.GlobalRef $(return (TH.LitT (TH.StrTyLit refName)))) |]
     WT.BaseBVRepr _ ->
       [| ARMGlobalBV (ASL.knownGlobalRef :: ASL.GlobalRef $(return (TH.LitT (TH.StrTyLit refName)))) |]
+    WT.BaseStructRepr Ctx.Empty ->
+      [| ARMDummyReg |]
     _tp -> [| error $ "locToRegTH undefined for unrecognized location: " <> $(return $ TH.LitE (TH.StringL refName)) |]
 
 branchTakenReg :: ARMReg MT.BoolType

macaw-aarch32/src/Data/Macaw/ARM/Arch.hs

@@ -161,7 +161,7 @@ data ARMPrimFn (f :: MT.Type -> Type) tp where
   FPRecipStep :: (1 <= w)
               => NR.NatRepr w
               -> f (MT.BVType w)
-              -> f (MT.BVType 32)
+              -> f (MT.BVType w)
               -> ARMPrimFn f (MT.BVType w)
   FPSqrtEstimate :: (1 <= w)
                  => NR.NatRepr w
@@ -171,7 +171,7 @@ data ARMPrimFn (f :: MT.Type -> Type) tp where
   FPRSqrtStep :: (1 <= w)
               => NR.NatRepr w
               -> f (MT.BVType w)
-              -> f (MT.BVType 32)
+              -> f (MT.BVType w)
               -> ARMPrimFn f (MT.BVType w)
   FPSqrt :: (1 <= w)
          => NR.NatRepr w

macaw-aarch32/src/Data/Macaw/ARM/Eval.hs

@@ -64,7 +64,6 @@ initialBlockRegs addr _preconds = MSG.initRegState addr &
   -- once we get Thumb support, we will want to refer to the semantics
   -- for this.
   MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ MC.BVValue knownNat 0 &
-  MC.boundValue AR.ARMWriteMode .~ MC.BVValue knownNat 0 &
   MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_IT")) .~ MC.BVValue knownNat 0 &
   MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_T")) .~ MC.BVValue knownNat 0 &
   MC.boundValue (AR.ARMGlobalBV (ASL.knownGlobalRef @"PSTATE_nRW")) .~ MC.BVValue knownNat 1 &

macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs

@@ -16,7 +16,7 @@ import qualified Data.ByteString as BS
 import qualified Data.List as L
 import           Data.Macaw.ARM.ARMReg ( locToRegTH )
 import           Data.Macaw.ARM.Arch ( a32InstructionMatcher )
-import           Data.Macaw.ARM.Semantics.TH ( armAppEvaluator, armNonceAppEval, loadSemantics )
+import           Data.Macaw.ARM.Semantics.TH ( armAppEvaluator, armNonceAppEval, loadSemantics, armTranslateType )
 import qualified Data.Macaw.CFG as MC
 import           Data.Macaw.SemMC.Generator ( Generator )
 import           Data.Macaw.SemMC.TH ( MacawTHConfig(..), genExecInstruction )
@@ -33,6 +33,7 @@ import qualified SemMC.Architecture.AArch32 as ARMSem
 import           SemMC.Architecture.ARM.Opcodes ( ASLSemantics(..), allA32OpcodeInfo )
 import qualified SemMC.Formula as SF
 import qualified What4.Expr.Builder as WEB
+import qualified What4.Interface as S
 
 execInstruction :: MC.Value ARMSem.AArch32 ids (MT.BVType 32)
                 -> Instruction
@@ -62,6 +63,7 @@ execInstruction =
                                   , archTypeQ = [t| ARMSem.AArch32 |]
                                   , genLibraryFunction = notVecLib
                                   , genOpcodeCase = notVecOpc
+                                  , archTranslateType = armTranslateType
                                   }
 
        genExecInstruction (Proxy @ARMSem.AArch32)

macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs

@@ -1,13 +1,16 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE DeriveLift #-}
+{-# LANGUAGE GADTs #-}
 module Data.Macaw.ARM.Semantics.TH
     ( armAppEvaluator
     , armNonceAppEval
@@ -16,6 +19,7 @@ module Data.Macaw.ARM.Semantics.TH
     , getSIMD
     , setSIMD
     , loadSemantics
+    , armTranslateType
     )
     where
 
@@ -27,12 +31,12 @@ import           Data.Macaw.ARM.ARMReg
 import           Data.Macaw.ARM.Arch
 import qualified Data.Macaw.CFG as M
 import qualified Data.Macaw.SemMC.Generator as G
-import           Data.Macaw.SemMC.TH ( addEltTH, natReprTH, symFnName )
+import           Data.Macaw.SemMC.TH ( addEltTH, natReprTH, symFnName, translateBaseTypeRepr )
 import           Data.Macaw.SemMC.TH.Monad
 import qualified Data.Macaw.Types as M
 import           Data.Parameterized.Classes
-import qualified Data.Parameterized.Classes as PC
 import qualified Data.Parameterized.Context as Ctx
+import qualified Data.Parameterized.TraversableFC as FC
 import           Data.Parameterized.NatRepr
 import           GHC.TypeLits as TL
 import qualified Lang.Crucible.Backend.Simple as CBS
@@ -72,13 +76,36 @@ armNonceAppEval bvi nonceApp =
         let fnName = symFnName symFn
             tp = WB.symFnReturnType symFn
         in case fnName of
+          -- NOTE: The state fields corresponding to the assertion
+          -- failure, undefined behavior and unpredictable behavior flags
+          -- are not used, and have been wrapped in the following 3 functions.
+          -- To save time, for now we can simply avoid translating them.
+          
+          "uf_update_assert" -> case args of
+            Ctx.Empty Ctx.:> _assertVar -> Just $ do
+              --assertVarE <- addEltTH M.LittleEndian bvi assertVar
+              --liftQ [| $(refBinding assertVarE) |]
+              liftQ [| return $ M.BoolValue False |]
+            _ -> fail "Invalid uf_update_assert"
+          "uf_update_undefB" -> case args of
+            Ctx.Empty Ctx.:> _undefVar -> Just $ do
+              --undefVarE <- addEltTH M.LittleEndian bvi undefVar
+              --liftQ [| $(refBinding undefVarE) |]
+              liftQ [| return $ M.BoolValue False |]
+            _ -> fail "Invalid uf_update_undefB"
+          "uf_update_unpredB" -> case args of
+            Ctx.Empty Ctx.:> _unpredVar -> Just $ do
+              --unpredVarE <- addEltTH M.LittleEndian bvi unpredVar
+              --liftQ [| $(refBinding unpredVarE) |]
+              liftQ [| return $ M.BoolValue False |]
+            _ -> fail "Invalid uf_update_unpredB"
           "uf_simd_set" ->
             case args of
               Ctx.Empty Ctx.:> rgf Ctx.:> rid Ctx.:> val -> Just $ do
                 rgfE <- addEltTH M.LittleEndian bvi rgf
                 ridE <- addEltTH M.LittleEndian bvi rid
                 valE <- addEltTH M.LittleEndian bvi val
-                liftQ [| join (setSIMD <$> $(refBinding rgfE) <*> $(refBinding ridE) <*> $(refBinding valE)) |]
+                liftQ $ joinOp3 [| setSIMD |] rgfE ridE valE
               _ -> fail "Invalid uf_simd_get"
           "uf_gpr_set" ->
             case args of
@@ -86,7 +113,7 @@ armNonceAppEval bvi nonceApp =
                 rgfE <- addEltTH M.LittleEndian bvi rgf
                 ridE <- addEltTH M.LittleEndian bvi rid
                 valE <- addEltTH M.LittleEndian bvi val
-                liftQ [| join (setGPR <$> $(refBinding rgfE) <*> $(refBinding ridE) <*> $(refBinding valE)) |]
+                liftQ $ joinOp3 [| setGPR |] rgfE ridE valE
               _ -> fail "Invalid uf_gpr_get"
           "uf_simd_get" ->
             case args of
@@ -94,7 +121,7 @@ armNonceAppEval bvi nonceApp =
                 Just $ do
                   _rgf <- addEltTH M.LittleEndian bvi array
                   rid <- addEltTH M.LittleEndian bvi ix
-                  liftQ [| getSIMD =<< $(refBinding rid) |]
+                  liftQ $ joinOp1 [| getSIMD |] rid
               _ -> fail "Invalid uf_simd_get"
           "uf_gpr_get" ->
             case args of
@@ -102,7 +129,7 @@ armNonceAppEval bvi nonceApp =
                 Just $ do
                   _rgf <- addEltTH M.LittleEndian bvi array
                   rid <- addEltTH M.LittleEndian bvi ix
-                  liftQ [| getGPR =<< $(refBinding rid) |]
+                  liftQ $ joinOp1 [| getGPR |] rid
               _ -> fail "Invalid uf_gpr_get"
           _ | "uf_write_mem_" `isPrefixOf` fnName ->
             case args of
@@ -113,16 +140,15 @@ armNonceAppEval bvi nonceApp =
                 addrE <- addEltTH M.LittleEndian bvi addr
                 valE <- addEltTH M.LittleEndian bvi val
                 let memWidth = fromIntegral (intValue memWidthRepr) `div` 8
-                liftQ [| join (writeMem <$> $(refBinding memE) <*> $(refBinding addrE) <*> pure $(natReprFromIntTH memWidth) <*> $(refBinding valE)) |]
+                liftQ $ joinOp3 [| writeMem $(natReprFromIntTH memWidth) |] memE addrE valE
               _ -> fail "invalid write_mem"
 
 
-
           _ | "uf_unsignedRSqrtEstimate" `isPrefixOf` fnName ->
               case args of
                 Ctx.Empty Ctx.:> op -> Just $ do
                   ope <- addEltTH M.LittleEndian bvi op
-                  liftQ [| G.addExpr =<< (UnsignedRSqrtEstimate knownNat <$> $(refBinding ope)) |]
+                  liftQ [| G.addExpr =<< $(joinOp1 [| \e1E -> addArchAssignment (UnsignedRSqrtEstimate knownNat e1E) |] ope) |]
                 _ -> fail "Invalid unsignedRSqrtEstimate arguments"
 
           -- NOTE: This must come before fpMul, since fpMul is a prefix of this
@@ -133,7 +159,8 @@ armNonceAppEval bvi nonceApp =
                   op2e <- addEltTH M.LittleEndian bvi op2
                   op3e <- addEltTH M.LittleEndian bvi op3
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPMulAdd knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< join ((\o1 o2 o3 o4 -> addArchAssignment (FPMulAdd knownNat o1 o2 o3 o4)) <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding fpcre))  |]
+
                 _ -> fail "Invalid fpMulAdd arguments"
 
 
@@ -143,7 +170,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPSub knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPSub knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpSub arguments"
           _ | "uf_fpAdd" `isPrefixOf` fnName ->
               case args of
@@ -151,7 +178,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPAdd knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPAdd knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpAdd arguments"
           _ | "uf_fpMul" `isPrefixOf` fnName ->
               case args of
@@ -159,7 +186,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPMul knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPMul knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpMul arguments"
           _ | "uf_fpDiv" `isPrefixOf` fnName ->
               case args of
@@ -167,7 +194,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPMul knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPDiv knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpDiv arguments"
 
           _ | "uf_fpMaxNum" `isPrefixOf` fnName ->
@@ -176,7 +203,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPMaxNum knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPMaxNum knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpMaxNum arguments"
           _ | "uf_fpMinNum" `isPrefixOf` fnName ->
               case args of
@@ -184,7 +211,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPMinNum knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPMinNum knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpMinNum arguments"
           _ | "uf_fpMax" `isPrefixOf` fnName ->
               case args of
@@ -192,7 +219,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPMax knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPMax knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpMax arguments"
           _ | "uf_fpMin" `isPrefixOf` fnName ->
               case args of
@@ -200,7 +227,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPMin knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPMin knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpMin arguments"
 
           _ | "uf_fpRecipEstimate" `isPrefixOf` fnName ->
@@ -208,35 +235,35 @@ armNonceAppEval bvi nonceApp =
                 Ctx.Empty Ctx.:> op1 Ctx.:> fpcr -> Just $ do
                   op1e <- addEltTH M.LittleEndian bvi op1
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPRecipEstimate knownNat <$> $(refBinding op1e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (FPRecipEstimate knownNat e1E e2E) |] op1e fpcre) |]
                 _ -> fail "Invalid fpRecipEstimate arguments"
           _ | "uf_fpRecipStep" `isPrefixOf` fnName ->
               case args of
-                Ctx.Empty Ctx.:> op1 Ctx.:> fpcr -> Just $ do
+                Ctx.Empty Ctx.:> op1 Ctx.:> op2 -> Just $ do
                   op1e <- addEltTH M.LittleEndian bvi op1
-                  fpcre <- addEltTH M.LittleEndian bvi fpcr
+                  op2e <- addEltTH M.LittleEndian bvi op2
-                  liftQ [| G.addExpr =<< (FPRecipStep knownNat <$> $(refBinding op1e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (FPRecipStep knownNat e1E e2E) |] op1e op2e) |]
                 _ -> fail "Invalid fpRecipStep arguments"
           _ | "uf_fpSqrtEstimate" `isPrefixOf` fnName ->
               case args of
                 Ctx.Empty Ctx.:> op1 Ctx.:> fpcr -> Just $ do
                   op1e <- addEltTH M.LittleEndian bvi op1
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPSqrtEstimate knownNat <$> $(refBinding op1e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (FPSqrtEstimate knownNat e1E e2E) |] op1e fpcre) |]
                 _ -> fail "Invalid fpSqrtEstimate arguments"
           _ | "uf_fprSqrtStep" `isPrefixOf` fnName ->
               case args of
                 Ctx.Empty Ctx.:> op1 Ctx.:> fpcr -> Just $ do
                   op1e <- addEltTH M.LittleEndian bvi op1
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPRSqrtStep knownNat <$> $(refBinding op1e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (FPRSqrtStep knownNat e1E e2E) |] op1e fpcre) |]
                 _ -> fail "Invalid fprSqrtStep arguments"
           _ | "uf_fpSqrt" `isPrefixOf` fnName ->
               case args of
                 Ctx.Empty Ctx.:> op1 Ctx.:> fpcr -> Just $ do
                   op1e <- addEltTH M.LittleEndian bvi op1
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPSqrt knownNat <$> $(refBinding op1e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (FPSqrt knownNat e1E e2E) |] op1e fpcre) |]
                 _ -> fail "Invalid fpSqrt arguments"
 
           _ | "uf_fpCompareGE" `isPrefixOf` fnName ->
@@ -245,7 +272,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPCompareGE knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPCompareGE knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpCompareGE arguments"
           _ | "uf_fpCompareGT" `isPrefixOf` fnName ->
               case args of
@@ -253,7 +280,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPCompareGT knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPCompareGT knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpCompareGT arguments"
           _ | "uf_fpCompareEQ" `isPrefixOf` fnName ->
               case args of
@@ -261,7 +288,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPCompareEQ knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPCompareEQ knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpCompareEQ arguments"
           _ | "uf_fpCompareNE" `isPrefixOf` fnName ->
               case args of
@@ -269,7 +296,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPCompareNE knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPCompareNE knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpCompareNE arguments"
           _ | "uf_fpCompareUN" `isPrefixOf` fnName ->
               case args of
@@ -277,7 +304,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   fpcre <- addEltTH M.LittleEndian bvi fpcr
-                  liftQ [| G.addExpr =<< (FPCompareUN knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding fpcre)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPCompareUN knownNat e1E e2E e3E) |] op1e op2e fpcre) |]
                 _ -> fail "Invalid fpCompareUN arguments"
 
           "uf_fpToFixedJS" ->
@@ -286,7 +313,7 @@ armNonceAppEval bvi nonceApp =
                 op1e <- addEltTH M.LittleEndian bvi op1
                 op2e <- addEltTH M.LittleEndian bvi op2
                 op3e <- addEltTH M.LittleEndian bvi op3
-                liftQ [| G.addExpr =<< (FPToFixedJS <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e)) |]
+                liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPToFixedJS e1E e2E e3E) |] op1e op2e op3e) |]
               _ -> fail "Invalid fpToFixedJS arguments"
           _ | "uf_fpToFixed" `isPrefixOf` fnName ->
               case args of
@@ -296,7 +323,7 @@ armNonceAppEval bvi nonceApp =
                   op3e <- addEltTH M.LittleEndian bvi op3
                   op4e <- addEltTH M.LittleEndian bvi op4
                   op5e <- addEltTH M.LittleEndian bvi op5
-                  liftQ [| G.addExpr =<< (FPToFixed knonwNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding op4e) <*> $(refBinding op5e)) |]
+                  liftQ [| G.addExpr =<< join ((\o1 o2 o3 o4 o5 -> addArchAssignment (FPToFixed knownNat o1 o2 o3 o4 o5)) <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding op4e) <*> $(refBinding op5e)) |]
                 _ -> fail "Invalid fpToFixed arguments"
           _ | "uf_fixedToFP" `isPrefixOf` fnName ->
               case args of
@@ -306,7 +333,7 @@ armNonceAppEval bvi nonceApp =
                   op3e <- addEltTH M.LittleEndian bvi op3
                   op4e <- addEltTH M.LittleEndian bvi op4
                   op5e <- addEltTH M.LittleEndian bvi op5
-                  liftQ [| G.addExpr =<< (FixedToFP knonwNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding op4e) <*> $(refBinding op5e)) |]
+                  liftQ [| G.addExpr =<< join ((\o1 o2 o3 o4 o5 -> addArchAssignment (FixedToFP knownNat o1 o2 o3 o4 o5)) <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding op4e) <*> $(refBinding op5e))  |]
                 _ -> fail "Invalid fixedToFP arguments"
           _ | "uf_fpConvert" `isPrefixOf` fnName ->
               case args of
@@ -314,7 +341,7 @@ armNonceAppEval bvi nonceApp =
                   op1e <- addEltTH M.LittleEndian bvi op1
                   op2e <- addEltTH M.LittleEndian bvi op2
                   op3e <- addEltTH M.LittleEndian bvi op3
-                  liftQ [| G.addExpr =<< (FPConvert knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e)) |]
+                  liftQ [| G.addExpr =<< $(joinOp3 [| \e1E e2E e3E -> addArchAssignment (FPConvert knownNat e1E e2E e3E) |] op1e op2e op3e) |]
                 _ -> fail "Invalid fpConvert arguments"
           _ | "uf_fpRoundInt" `isPrefixOf` fnName ->
               case args of
@@ -323,79 +350,42 @@ armNonceAppEval bvi nonceApp =
                   op2e <- addEltTH M.LittleEndian bvi op2
                   op3e <- addEltTH M.LittleEndian bvi op3
                   op4e <- addEltTH M.LittleEndian bvi op4
-                  liftQ [| G.addExpr =<< (FPRoundInt knownNat <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding op4e)) |]
+                  liftQ [| G.addExpr =<< join ((\o1 o2 o3 o4 -> addArchAssignment (FPRoundInt knownNat o1 o2 o3 o4)) <$> $(refBinding op1e) <*> $(refBinding op2e) <*> $(refBinding op3e) <*> $(refBinding op4e))  |]
                 _ -> fail "Invalid fpRoundInt arguments"
 
-          -- NOTE: These three cases occasionally end up unused.  Because we let
+
-          -- bind almost everything, that can lead to the 'arch' type parameter
+          "uf_init_gprs" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteGPRs) |]
-          -- being ambiguous, which is an error for various reasons.
+          "uf_init_memory" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteMemory)|]
-          --
+          "uf_init_simds" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteSIMDs) |]
-          -- To fix that, we add an explicit type application here.
-          "uf_init_gprs" -> Just $ liftQ [| M.AssignedValue <$> G.addAssignment @ARM.AArch32 (M.SetUndefined $(what4TypeTH tp)) |]
-          "uf_init_memory" -> Just $ liftQ [| M.AssignedValue <$> G.addAssignment @ARM.AArch32 (M.SetUndefined $(what4TypeTH tp)) |]
-          "uf_init_simds" -> Just $ liftQ [| M.AssignedValue <$> G.addAssignment @ARM.AArch32 (M.SetUndefined $(what4TypeTH tp)) |]
 
 
-          -- NOTE: These cases are tricky because they generate groups of
+          -- These functions indicate that the wrapped monadic actions in the corresponding
-          -- statements that need to behave a bit differently in (eager)
+          -- 'ARMWriteAction' should be executed, committing their stateful actions.
-          -- top-level code generation and (lazy) conditional code generation.
-          --
-          -- In either case, the calls to 'setWriteMode' /must/ bracket the
-          -- memory/register update function.
-          --
-          -- In the eager translation case, that means that we have to lexically
-          -- emit the update between the write mode guards (so that the effect
-          -- actually happens).
-          --
-          -- In contrast, the lazy translation case has to emit the write
-          -- operation as a lazy let binding to preserve sharing, but group all
-          -- three statements in the actual 'Generator' monad.
           "uf_update_gprs"
             | Ctx.Empty Ctx.:> gprs <- args -> Just $ do
-              istl <- isTopLevel
+                gprs' <- addEltTH M.LittleEndian bvi gprs
-              case istl of
+                appendStmt $ [| join (execWriteAction <$> $(refBinding gprs')) |]
-                False -> do
+                liftQ [| return $ unitValue |]
-                  gprs' <- addEltTH M.LittleEndian bvi gprs
+                  
-                  liftQ [| do setWriteMode WriteGPRs
-                              $(refBinding gprs')
-                              setWriteMode WriteNone
-                         |]
-                True -> do
-                  appendStmt [| setWriteMode WriteGPRs |]
-                  gprs' <- addEltTH M.LittleEndian bvi gprs
-                  appendStmt [| setWriteMode WriteNone |]
-                  extractBound gprs'
           "uf_update_simds"
             | Ctx.Empty Ctx.:> simds <- args -> Just $ do
-                istl <- isTopLevel
+                simds' <- addEltTH M.LittleEndian bvi simds
-                case istl of
+                appendStmt $ [| join (execWriteAction <$> $(refBinding simds')) |]
-                  False -> do
+                liftQ [| return $ unitValue |]
-                    simds' <- addEltTH M.LittleEndian bvi simds
+
-                    liftQ [| do setWriteMode WriteSIMDs
-                                $(refBinding simds')
-                                setWriteMode WriteNone
-                           |]
-                  True -> do
-                    appendStmt [| setWriteMode WriteSIMDs |]
-                    simds' <- addEltTH M.LittleEndian bvi simds
-                    appendStmt [| setWriteMode WriteNone |]
-                    extractBound simds'
           "uf_update_memory"
             | Ctx.Empty Ctx.:> mem <- args -> Just $ do
-                istl <- isTopLevel
+                mem' <- addEltTH M.LittleEndian bvi mem
-                case istl of
+                appendStmt $ [| join (execWriteAction <$> $(refBinding mem')) |]
-                  False -> do
+                liftQ [| return $ unitValue |]
-                    mem' <- addEltTH M.LittleEndian bvi mem
-                    liftQ [| do setWriteMode WriteMemory
-                                $(refBinding mem')
-                                setWriteMode WriteNone
-                           |]
-                  True -> do
-                    appendStmt [| setWriteMode WriteMemory |]
-                    mem' <- addEltTH M.LittleEndian bvi mem
-                    appendStmt [| setWriteMode WriteNone |]
-                    extractBound mem'
 
+          "uf_noop" | Ctx.Empty <- args -> Just $ liftQ [| return $ M.BoolValue True |]
+
+          "uf_join_units"
+            | Ctx.Empty Ctx.:> u1 Ctx.:> u2 <- args -> Just $ do
+                _ <- addEltTH M.LittleEndian bvi u1
+                _ <- addEltTH M.LittleEndian bvi u2
+                liftQ [| return $ unitValue |]
           _ | "uf_assertBV_" `isPrefixOf` fnName ->
             case args of
               Ctx.Empty Ctx.:> assert Ctx.:> bv -> Just $ do
@@ -411,71 +401,56 @@ armNonceAppEval bvi nonceApp =
               _ -> fail "Invalid call to assertBV"
 
           _ | "uf_UNDEFINED_" `isPrefixOf` fnName ->
-               Just $ liftQ [| M.AssignedValue <$> G.addAssignment (M.SetUndefined $(what4TypeTH tp)) |]
+               Just $ liftQ [| M.AssignedValue <$> G.addAssignment (M.SetUndefined $(translateBaseTypeRepr tp)) |]
           _ | "uf_INIT_GLOBAL_" `isPrefixOf` fnName ->
-               Just $ liftQ [| M.AssignedValue <$> G.addAssignment (M.SetUndefined $(what4TypeTH tp)) |]
+               Just $ liftQ [| M.AssignedValue <$> G.addAssignment (M.SetUndefined $(translateBaseTypeRepr tp)) |]
           _ -> Nothing
       _ -> Nothing -- fallback to default handling
 
+
+unitValue :: M.Value ARM.AArch32 ids (M.TupleType '[])
+unitValue =  M.Initial ARMDummyReg
+
 natReprFromIntTH :: Int -> Q Exp
 natReprFromIntTH i = [| knownNat :: M.NatRepr $(litT (numTyLit (fromIntegral i))) |]
 
-data WriteMode =
-  WriteNone
-  | WriteGPRs
-  | WriteSIMDs
-  | WriteMemory
-  deriving (Show, Eq, Lift)
 
-getWriteMode :: G.Generator ARM.AArch32 ids s WriteMode
+data ARMWriteGPRs = ARMWriteGPRs
-getWriteMode = do
+data ARMWriteMemory = ARMWriteMemory
-  G.getRegVal ARMWriteMode >>= \case
+data ARMWriteSIMDs = ARMWriteSIMDs
-      M.BVValue _ i -> return $ case i of
-        0 -> WriteNone
-        1 -> WriteGPRs
-        2 -> WriteSIMDs
-        3 -> WriteMemory
-        _ -> error "impossible"
-      _ -> error "impossible"
 
-setWriteMode :: WriteMode -> G.Generator ARM.AArch32 ids s ()
+newtype ARMWriteAction ids s tp where
-setWriteMode wm =
+  ARMWriteAction :: G.Generator ARM.AArch32 ids s tp -> ARMWriteAction ids s tp
-  let
+  deriving (Functor, Applicative, Monad)
-    i = case wm of
+
-      WriteNone -> 0
+execWriteAction :: ARMWriteAction ids s tp -> G.Generator ARM.AArch32 ids s tp
-      WriteGPRs -> 1
+execWriteAction (ARMWriteAction f) = f
-      WriteSIMDs -> 2
-      WriteMemory -> 3
-  in G.setRegVal ARMWriteMode (M.BVValue knownNat i)
 
 writeMem :: 1 <= w
-         => M.Value ARM.AArch32 ids tp
+         => M.NatRepr w
+         -> ARMWriteAction ids s ARMWriteMemory
          -> M.Value ARM.AArch32 ids (M.BVType 32)
-         -> M.NatRepr w
          -> M.Value ARM.AArch32 ids (M.BVType (8 TL.* w))
-         -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids tp)
+         -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s ARMWriteMemory)
-writeMem mem addr sz val = do
+writeMem sz mem addr val = return $ do
-  wm <- getWriteMode
+  _ <- mem
-  case wm of
+  ARMWriteAction $ G.addStmt (M.WriteMem addr (M.BVMemRepr sz M.LittleEndian) val)
-    WriteMemory -> do
+  return $ ARMWriteMemory
-      G.addStmt (M.WriteMem addr (M.BVMemRepr sz M.LittleEndian) val)
-      return mem
-    _ -> return mem
 
-setGPR :: M.Value ARM.AArch32 ids tp
+setGPR :: ARMWriteAction ids s ARMWriteGPRs
        -> M.Value ARM.AArch32 ids (M.BVType 4)
        -> M.Value ARM.AArch32 ids (M.BVType 32)
-       -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids tp)
+       -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s ARMWriteGPRs)
 setGPR handle regid v = do
   reg <- case regid of
     M.BVValue w i
       | intValue w == 4
       , Just reg <- integerToReg i -> return reg
     _ -> E.throwError (G.GeneratorMessage $ "Bad GPR identifier (uf_gpr_set): " <> show (M.ppValueAssignments v))
-  getWriteMode >>= \case
+  return $ do
-    WriteGPRs -> G.setRegVal reg v
+    _ <- handle
-    _ -> return ()
+    ARMWriteAction $ G.setRegVal reg v
-  return handle
+    return $ ARMWriteGPRs
 
 getGPR :: M.Value ARM.AArch32 ids tp
        -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids (M.BVType 32))
@@ -487,20 +462,21 @@ getGPR v = do
     _ ->  E.throwError (G.GeneratorMessage $ "Bad GPR identifier (uf_gpr_get): " <> show (M.ppValueAssignments v))
   G.getRegSnapshotVal reg
 
-setSIMD :: M.Value ARM.AArch32 ids tp
+setSIMD :: ARMWriteAction ids s ARMWriteSIMDs
-       -> M.Value ARM.AArch32 ids (M.BVType 8)
+        -> M.Value ARM.AArch32 ids (M.BVType 8)
-       -> M.Value ARM.AArch32 ids (M.BVType 128)
+        -> M.Value ARM.AArch32 ids (M.BVType 128)
-       -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids tp)
+        -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s ARMWriteSIMDs)
 setSIMD handle regid v = do
   reg <- case regid of
     M.BVValue w i
       | intValue w == 8
       , Just reg <- integerToSIMDReg i -> return reg
     _ -> E.throwError (G.GeneratorMessage $ "Bad SIMD identifier (uf_simd_set): " <> show (M.ppValueAssignments v))
-  getWriteMode >>= \case
+  return $ do
-    WriteSIMDs -> G.setRegVal reg v
+    _ <- handle
-    _ -> return ()
+    ARMWriteAction $ G.setRegVal reg v
-  return handle
+    return $ ARMWriteSIMDs
+
 
 getSIMD :: M.Value ARM.AArch32 ids tp
        -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids (M.BVType 128))
@@ -510,13 +486,7 @@ getSIMD v = do
       | intValue w == 8
       , Just reg <- integerToSIMDReg i -> return reg
     _ ->  E.throwError (G.GeneratorMessage $ "Bad SIMD identifier (uf_simd_get): " <> show (M.ppValueAssignments v))
-  G.getRegVal reg
+  G.getRegSnapshotVal reg
-
-what4TypeTH :: WT.BaseTypeRepr tp -> Q Exp
-what4TypeTH (WT.BaseBVRepr natRepr) = [| M.BVTypeRepr $(natReprTH natRepr) |]
-what4TypeTH WT.BaseBoolRepr = [| M.BoolTypeRepr |]
-what4TypeTH tp = error $ "Unsupported base type: " <> show tp
-
 
 -- ----------------------------------------------------------------------
 
@@ -536,33 +506,17 @@ isPlaceholderType tp = case tp of
   _ | Just Refl <- testEquality tp (knownRepr :: WT.BaseTypeRepr ASL.AllSIMDBaseType) -> True
   _ -> False
 
--- | This combinator provides conditional evaluation of its branches
+-- | For placeholder types, we can't translate them into a Mux, and so we
---
+-- need to rely on the conditional being resolved to a concrete value so
--- Many conditionals in the semantics are translated as muxes (effectively
+-- we can translate it into a haskell if-then-else.
--- if-then-else expressions).  This is great most of the time, but problematic
+
--- if the branches include side effects (e.g., memory writes).  We only want
+concreteIte :: M.Value ARM.AArch32 ids (M.BoolType)
--- side effects to happen if the condition really is true.
+            -> a
---
+            -> a
--- This combinator checks to see if the condition is concretely true or false
+            -> a
--- (as expected) and then evaluates the corresponding 'G.Generator' action.
+concreteIte v t f = case v of
---
--- It is meant to be used in a context like:
---
--- > val <- concreteIte condition trueThings falseThings
---
--- where @condition@ has type Value and the branches have type 'G.Generator'
--- 'M.Value' (i.e., the branches get to return a value).
---
--- NOTE: This function panics (and throws an error) if the argument is not
--- concrete.
-concreteIte :: M.TypeRepr tp
-            -> M.Value ARM.AArch32 ids (M.BoolType)
-            -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids tp)
-            -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids tp)
-            -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids tp)
-concreteIte rep v t f = case v of
   M.CValue (M.BoolCValue b) -> if b then t else f
-  _ -> G.addExpr =<< G.AppExpr <$> (M.Mux rep v <$> t <*> f)
+  _ -> error "concreteIte: value must be concrete"
 
 -- | A smart constructor for division
 --
@@ -583,6 +537,57 @@ sdiv repr dividend divisor =
           in G.ValueExpr <$> G.addExpr (G.AppExpr app)
     _ -> addArchAssignment (SDiv repr dividend divisor)
 
+
+mkTupT :: [TypeQ] -> Q Type
+mkTupT [t] = t
+mkTupT ts = foldl appT (tupleT (length ts)) ts
+
+
+
+armTranslateType :: Q Type
+                 -> Q Type
+                 -> WT.BaseTypeRepr tp
+                 -> Maybe (Q Type)
+armTranslateType idsTy sTy tp = case tp of
+  WT.BaseStructRepr reprs -> Just $ mkTupT $ FC.toListFC translateBaseType reprs
+  _ | isPlaceholderType tp -> Just $ translateBaseType tp
+  _ -> Nothing
+  where
+    translateBaseType :: forall tp'. WT.BaseTypeRepr tp' -> Q Type
+    translateBaseType tp' =  case tp' of
+      _ | Just Refl <- testEquality tp' (knownRepr :: WT.BaseTypeRepr ASL.MemoryBaseType) ->
+          [t| ARMWriteAction $(idsTy) $(sTy) ARMWriteMemory |]
+      _ | Just Refl <- testEquality tp' (knownRepr :: WT.BaseTypeRepr ASL.AllSIMDBaseType) ->
+          [t| ARMWriteAction $(idsTy) $(sTy) ARMWriteSIMDs |]
+      _ | Just Refl <- testEquality tp' (knownRepr :: WT.BaseTypeRepr ASL.AllGPRBaseType) ->
+          [t| ARMWriteAction $(idsTy) $(sTy) ARMWriteGPRs |]
+      WT.BaseBoolRepr -> [t| M.Value ARM.AArch32 $(idsTy) M.BoolType |]
+      WT.BaseBVRepr n -> [t| M.Value ARM.AArch32 $(idsTy) (M.BVType $(litT (numTyLit (intValue n)))) |]
+      _ -> fail $ "unsupported base type: " ++ show tp
+
+extractTuple :: Int -> Int -> Q Exp
+extractTuple len i = do
+  nm <- newName "x"
+  let pat = tupP $ [ if i' == i then varP nm else wildP | i' <- [0..len-1] ]
+  lamE [pat] (varE nm)
+
+joinTuple :: [ExpQ] -> Q Exp
+joinTuple es = go [] es
+  where
+    go :: [Name] -> [ExpQ] -> Q Exp
+    go ns (e : es') = do
+      n <- newName "bval"
+      [| $(e) >>= $(lamE [varP n] (go (n : ns) es')) |]
+    go ns [] = [| return $(tupE $ map varE (reverse ns)) |]
+
+refField :: Ctx.Size ctx -> Ctx.Index ctx tp -> BoundExp -> MacawQ arch t fs BoundExp
+refField sz idx e = case Ctx.viewSize sz of
+  Ctx.IncSize sz' | Ctx.ZeroSize <- Ctx.viewSize sz' -> return e
+  _ -> case e of
+    EagerBoundExp (TupE es) | Ctx.indexVal idx < length es -> return $ EagerBoundExp $ es !! (Ctx.indexVal idx)
+    EagerBoundExp _ -> bindTH [| $(extractTuple (Ctx.sizeInt sz) (Ctx.indexVal idx)) $(refEager e) |]
+    LazyBoundExp _ -> letTH [| $(extractTuple (Ctx.sizeInt sz) (Ctx.indexVal idx)) <$> $(refBinding e) |]
+
 armAppEvaluator :: M.Endianness
                 -> BoundVarInterpretations ARM.AArch32 t fs
                 -> WB.App (WB.Expr t) ctp
@@ -590,41 +595,60 @@ armAppEvaluator :: M.Endianness
 armAppEvaluator endianness interps elt =
     case elt of
       WB.BaseIte bt _ test t f | isPlaceholderType bt -> return $ do
-        -- NOTE: This case is very special.  The placeholder types denote
+        -- In this case, the placeholder type indicates that
-        -- conditionals that are guarding the state update functions with
+        -- expression is to be translated as a (wrapped) stateful action
-        -- mutation.
+        -- rather than an actual macaw term. This is therefore translated
-        --
+        -- as a Haskell if-then-else statement, rather than
-        -- We need to ensure that state updates are only done lazily.  This
+        -- a Mux.
-        -- works because the arguments to the branches are expressions in the
-        -- Generator monad.  We can do this translation while preserving sharing
-        -- by turning every recursively-traversed term into a let binding at the
-        -- top-level.  After that, we can build bodies for the "arms" of the
-        -- concreteIte that instantiate those terms in the appropriate monadic
-        -- context.  It is slightly problematic that the core TH translation
-        -- doesn't really support that because it wants to (more efficiently)
-        -- evaluate all of the monadic stuff.  However, we don't need quite as
-        -- much generality for this code, so maybe a smaller core that just does
-        -- all of the necessary applicative binding of 'Generator' terms will be
-        -- sufficient.
         testE <- addEltTH endianness interps test
-        inConditionalContext $ do
+        tE <- addEltTH endianness interps t
-          tE <- addEltTH endianness interps t
+        fE <- addEltTH endianness interps f
-          fE <- addEltTH endianness interps f
+        case all isEager [testE, tE, fE] of
-          liftQ [| join (concreteIte PC.knownRepr <$> $(refBinding testE) <*> (return $(refBinding tE)) <*> (return $(refBinding fE))) |]
+          True -> liftQ [| return $ concreteIte $(refEager testE) $(refEager tE) $(refEager fE) |]
+          False -> liftQ [| concreteIte <$> $(refBinding testE) <*> $(refBinding tE) <*> $(refBinding fE) |]
+      WB.StructField struct _ _ |
+          (WT.BaseStructRepr (Ctx.Empty Ctx.:> _)) <- WB.exprType struct -> Just $ do
+        structE <- addEltTH endianness interps struct
+        extractBound structE
+      WB.StructField struct idx _ -> Just $ do
+        WT.BaseStructRepr reprs <- return $ WB.exprType struct
+        bnd <- lookupElt struct >>= \case
+          Just bnd -> return bnd
+          Nothing -> do
+            bnd <- addEltTH endianness interps struct
+            case isEager bnd of
+              True -> do
+                nms <- sequence $ FC.toListFC (\_ -> liftQ (newName "lval")) reprs
+                letBindPat struct (tupP $ map varP nms, tupE $ map varE nms) (refEager bnd)
+                res <- liftQ $ tupE $ map varE nms
+                return $ EagerBoundExp res
+              False -> return bnd
+        
+        fldBnd <- refField (Ctx.size reprs) idx bnd
+        extractBound fldBnd
+      WB.StructCtor _ (Ctx.Empty Ctx.:> e) -> Just $ do
+        bnd <- addEltTH endianness interps e
+        extractBound bnd
+
+      WB.StructCtor _ flds -> Just $ do
+        fldEs <- sequence $ FC.toListFC (addEltTH endianness interps) flds
+        case all isEager fldEs of
+          True -> liftQ $ [| return $(tupE (map refEager fldEs)) |]
+          False -> liftQ $ joinTuple (map refBinding fldEs)            
+            
       WB.BVSdiv w bv1 bv2 -> return $ do
         e1 <- addEltTH endianness interps bv1
         e2 <- addEltTH endianness interps bv2
-        liftQ [| G.addExpr =<< join (sdiv $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2)) |]
+        liftQ [| G.addExpr =<< $(joinOp2 [| sdiv $(natReprTH w) |] e1 e2) |]
       WB.BVUrem w bv1 bv2 -> return $ do
         e1 <- addEltTH endianness interps bv1
         e2 <- addEltTH endianness interps bv2
-        liftQ [| G.addExpr =<< join (addArchAssignment <$> (URem $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2)))
+        liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (URem $(natReprTH w) e1E e2E) |] e1 e2) |]
-               |]
+               
       WB.BVSrem w bv1 bv2 -> return $ do
         e1 <- addEltTH endianness interps bv1
         e2 <- addEltTH endianness interps bv2
-        liftQ [| G.addExpr =<< join (addArchAssignment <$> (SRem $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2)))
+        liftQ [| G.addExpr =<< $(joinOp2 [| \e1E e2E -> addArchAssignment (SRem $(natReprTH w) e1E e2E) |] e1 e2) |]
-               |]
       WB.IntegerToBV _ _ -> return $ liftQ [| error "IntegerToBV" |]
       WB.SBVToInteger _ -> return $ liftQ [| error "SBVToInteger" |]
       WB.BaseIte bt _ test t f ->

macaw-aarch32/src/Data/Macaw/ARM/Simplify.hs

@@ -24,7 +24,9 @@ instance MSS.SimplifierExtension ARM.AArch32 where
                       coalesceAdditionByConstant a <|>
                       simplifyNestedMux a <|>
                       distributeAddOverConstantMux a <|>
-                      doubleNegation a
+                      doubleNegation a <|>
+                      negatedTrivialMux a <|>
+                      negatedMux a
   simplifyArchFn = armSimplifyArchFn
 
 armSimplifyArchFn :: MC.ArchFn ARM.AArch32 (MC.Value ARM.AArch32 ids) tp
@@ -154,4 +156,21 @@ doubleNegation app = do
   MC.NotApp r2 <- MC.valueAsApp r1
   MC.valueAsApp r2
 
+
+negatedTrivialMux :: MC.App (MC.Value ARM.AArch32 ids) tp
+                  -> Maybe (MC.App (MC.Value ARM.AArch32 ids) tp)
+negatedTrivialMux app = case app of
+  MC.Mux _ cond (MC.BoolValue False) (MC.BoolValue True) ->
+    case MSS.simplifyArchApp (MC.NotApp cond) of
+      Just app' -> return app'
+      _ -> return $ MC.NotApp cond
+  _ -> Nothing
+
+negatedMux :: MC.App (MC.Value ARM.AArch32 ids) tp
+           -> Maybe (MC.App (MC.Value ARM.AArch32 ids) tp)
+negatedMux app = do
+  MC.Mux rep c l r <- return app
+  MC.NotApp c' <- MC.valueAsApp c
+  return $ MC.Mux rep c' r l
+
 -- Potentially Normalize negations?

macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs

@@ -54,6 +54,7 @@ execInstruction =
                                   , archTypeQ = [t| (SP.AnyPPC SP.V32) |]
                                   , genLibraryFunction = \_ -> True
                                   , genOpcodeCase = genOpc
+                                  , archTranslateType = \_ _ _ -> Nothing
                                   }
 
        genExecInstruction proxy

macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs

@@ -55,6 +55,7 @@ execInstruction =
                                   , archTypeQ = [t| (SP.AnyPPC SP.V64) |]
                                   , genLibraryFunction = \_ -> True
                                   , genOpcodeCase = genOpc
+                                  , archTranslateType = \_ _ _ -> Nothing
                                   }
 
        genExecInstruction proxy

macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs

@@ -96,6 +96,8 @@ simplifyApp a =
     BVUnsignedLt v1 v2                -> unsignedRelOp (<) v1 v2
     Mux _ _ t f
       | Just Refl <- testEquality t f -> Just t
+    Mux _ c (BoolValue True) (BoolValue False) -> Just c
+    Mux _ c (BoolValue False) (BoolValue True) -> simplifyApp (NotApp c)
     _                                 -> Nothing
   where
     unop :: forall n . (tp ~ BVType n)

macaw-semmc/src/Data/Macaw/SemMC/TH.hs

@@ -36,18 +36,21 @@ module Data.Macaw.SemMC.TH (
   floatInfoTH,
   floatInfoFromPrecisionTH,
   symFnName,
-  asName
+  asName,
+  translateBaseType,
+  translateBaseTypeRepr
   ) where
 
 import           GHC.TypeLits ( Symbol )
 
 import           Control.Lens ( (^.) )
-import           Control.Monad ( ap, join, void )
+import           Control.Monad ( ap, join, void, liftM, foldM, forM )
 import qualified Control.Concurrent.Async as Async
 import qualified Data.Functor.Const as C
 import           Data.Functor.Product
 import qualified Data.Foldable as F
 import qualified Data.List as L
+import qualified Data.List.NonEmpty as NE
 import qualified Data.Map as Map
 import           Data.Maybe ( fromMaybe )
 import           Data.Proxy ( Proxy(..) )
@@ -568,11 +571,12 @@ translateFunction thConf fnName df ff = do
   idsTy <- varT <$> newName "ids"
   sTy <- varT <$> newName "s"
   let translate :: forall tp. CT.BaseTypeRepr tp -> Q Type
-      translate tp =
+      translate tp = case archTranslateType thConf idsTy sTy tp of
-        [t| M.Value $(archTypeQ thConf) $(idsTy) $(translateBaseType tp) |]
+        Just t -> t
+        Nothing -> [t| M.Value $(archTypeQ thConf) $(idsTy) $(translateBaseType tp) |]
+         
       argHsTys = FC.toListFC translate (ffArgTypes ff)
-      retHsTy = [t| G.Generator $(archTypeQ thConf) $(idsTy) $(sTy)
+      retHsTy = [t| G.Generator $(archTypeQ thConf) $(idsTy) $(sTy) $(translate (ffRetType ff)) |]
-                     $(translate (ffRetType ff)) |]
       ty = foldr (\a r -> [t| $(a) -> $(r) |]) retHsTy argHsTys
       body = doE (map return stmts)
   sig <- sigD var ty
@@ -580,10 +584,16 @@ translateFunction thConf fnName df ff = do
   return (var, sig, def)
 
 translateBaseType :: CT.BaseTypeRepr tp -> Q Type
-translateBaseType tp =
+translateBaseType tp =  case tp of
+  CT.BaseBoolRepr -> [t| M.BoolType |]
+  CT.BaseBVRepr n -> appT [t| M.BVType |] (litT (numTyLit (intValue n)))
+  _ -> fail $ "unsupported base type: " ++ show tp
+
+translateBaseTypeRepr :: CT.BaseTypeRepr tp -> Q Exp
+translateBaseTypeRepr tp =
   case tp of
-    CT.BaseBoolRepr -> [t| M.BoolType |]
+    CT.BaseBoolRepr -> [| M.BoolTypeRepr |]
-    CT.BaseBVRepr n -> appT [t| M.BVType |] (litT (numTyLit (intValue n)))
+    CT.BaseBVRepr n -> [| M.BVTypeRepr $(natReprTH n) |]
     _ -> fail $ "unsupported base type: " ++ show tp
 
 -- | wrapper around bitvector constants that forces some type
@@ -616,7 +626,10 @@ addEltTH endianness interps elt = do
           -- for now.  Once that works, we can be smarter and translate what we
           -- can eagerly.
           genExpr <- appToExprTH endianness (S.appExprApp appElt) interps
-          letBindExpr elt genExpr
+          istl <- isTopLevel
+          if istl
+            then bindExpr elt (return genExpr)
+            else letBindExpr elt genExpr
         S.BoundVarExpr bVar -> do
           x <- evalBoundVar interps bVar
           letBindPureExpr elt [| $(return x) |]
@@ -655,7 +668,7 @@ evalBoundVar interps bVar =
        return (VarE name)
      | otherwise -> fail $ "bound var not found: " ++ show bVar
 
-symFnName :: S.ExprSymFn t args ret -> String
+symFnName :: S.ExprSymFn t (S.Expr t) args ret -> String
 symFnName = T.unpack . Sy.solverSymbolAsText . S.symFnName
 
 bvarName :: S.ExprBoundVar t tp -> String
@@ -666,7 +679,7 @@ bvarName = T.unpack . Sy.solverSymbolAsText . S.bvarName
 writeMemTH :: forall arch t fs args ret
             . (A.Architecture arch)
            => BoundVarInterpretations arch t fs
-           -> S.ExprSymFn t args ret
+           -> S.ExprSymFn t (S.Expr t) args ret
            -> Ctx.Assignment (S.Expr t) args
            -> M.Endianness
            -> MacawQ arch t fs (Some (S.Expr t))
@@ -726,10 +739,11 @@ defaultNonceAppEvaluator endianness bvi nonceApp =
       case funMaybe of
         Just fun -> do
           argExprs <- sequence $ FC.toListFC (addEltTH endianness bvi) args
-          let applyQ e be = [| $(e) `ap` $(refBinding be) |]
+          case all isEager argExprs of
-          -- FIXME: Check if all argExprs are 'EagerBoundExp's; if so, generate
+            True -> liftQ $ foldl appE (return fun) (map refEager argExprs)
-          -- a pure let bound version instead
+            False -> do
-          liftQ [| join $(foldl applyQ [| return $(return fun) |] argExprs) |]
+              let applyQ e be = [| $(e) `ap` $(refBinding be) |]
+              liftQ [| join $(foldl applyQ [| return $(return fun) |] argExprs) |]
         _ -> do
           let fnArgTypes = S.symFnArgTypes symFn
               fnRetType = S.symFnReturnType symFn
@@ -834,27 +848,27 @@ defaultAppEvaluator :: (A.Architecture arch)
 defaultAppEvaluator endianness elt interps = case elt of
   S.NotPred bool -> do
     e <- addEltTH endianness interps bool
-    liftQ [| addApp =<< (M.NotApp <$> $(refBinding e)) |]
+    liftQ $ joinPure1 [| addApp |] [| M.NotApp |] e
-  S.ConjPred boolmap -> evalBoolMap endianness interps AndOp True boolmap >>= extractBound
+  S.ConjPred boolmap -> do
+    l <- boolMapList (addEltTH endianness interps) boolmap
+    case all (\(bnd,_) -> isEager bnd) l of
+      True -> do
+        tms <- liftQ $ listE $ map (\(bnd, b) -> (tupE [refEager bnd, lift b])) l
+        liftQ [| allPreds $(return tms) |]
+      False -> do
+        tms <- liftQ $ listE $ map (\(bnd, b) -> (tupE [refBinding bnd, lift b])) l
+        liftQ [| joinPreds $(return tms) |]
   S.BaseIte bt _ test t f -> do
     -- FIXME: Generate code that dynamically checks for a concrete condition and
     -- make an ite instead of a mux if possible
+
     testE <- addEltTH endianness interps test
     tE <- addEltTH endianness interps t
     fE <- addEltTH endianness interps f
     case bt of
-      CT.BaseBoolRepr -> liftQ [| addApp =<<
+      CT.BaseBoolRepr -> liftQ $ joinPure3 [| addApp |] [| M.Mux M.BoolTypeRepr |] testE tE fE
-                                   (M.Mux M.BoolTypeRepr <$>
+      CT.BaseBVRepr w -> liftQ $ joinPure3 [| addApp |] [| M.Mux (M.BVTypeRepr $(natReprTH w)) |] testE tE fE
-                                    $(refBinding testE) <*> $(refBinding tE) <*> $(refBinding fE))
+      CT.BaseFloatRepr fpp -> liftQ $ joinPure3 [| addApp |] [| M.Mux (M.FloatTypeRepr $(floatInfoFromPrecisionTH fpp)) |] testE tE fE
-                                |]
-      CT.BaseBVRepr w -> liftQ [| addApp =<<
-                                   (M.Mux (M.BVTypeRepr $(natReprTH w)) <$>
-                                    $(refBinding testE) <*> $(refBinding tE) <*> $(refBinding fE))
-                                |]
-      CT.BaseFloatRepr fpp -> liftQ [| addApp =<<
-                                        (M.Mux (M.FloatTypeRepr $(floatInfoFromPrecisionTH fpp)) <$>
-                                         $(refBinding testE) <*> $(refBinding tE) <*> $(refBinding fE))
-                                     |]
       CT.BaseNatRepr -> liftQ [| error "Macaw semantics for nat ITE unsupported" |]
       CT.BaseIntegerRepr -> liftQ [| error "Macaw semantics for integer ITE unsupported" |]
       CT.BaseRealRepr -> liftQ [| error "Macaw semantics for real ITE unsupported" |]
@@ -866,27 +880,27 @@ defaultAppEvaluator endianness elt interps = case elt of
   S.BaseEq _bt bv1 bv2 -> do
     e1 <- addEltTH endianness interps bv1
     e2 <- addEltTH endianness interps bv2
-    liftQ [| addApp =<< (M.Eq <$> $(refBinding e1) <*> $(refBinding e2)) |]
+    liftQ $ joinPure2 [| addApp |] [| M.Eq |] e1 e2
   S.BVSlt bv1 bv2 -> do
     e1 <- addEltTH endianness interps bv1
     e2 <- addEltTH endianness interps bv2
-    liftQ [| addApp =<< (M.BVSignedLt <$> $(refBinding e1) <*> $(refBinding e2)) |]
+    liftQ $ joinPure2 [| addApp |] [| M.BVSignedLt |] e1 e2
   S.BVUlt bv1 bv2 -> do
     e1 <- addEltTH endianness interps bv1
     e2 <- addEltTH endianness interps bv2
-    liftQ [| addApp =<< (M.BVUnsignedLt <$> $(refBinding e1) <*> $(refBinding e2)) |]
+    liftQ $ joinPure2 [| addApp |] [| M.BVUnsignedLt |] e1 e2
   S.BVConcat w bv1 bv2 -> do
     let u = S.bvWidth bv1
         v = S.bvWidth bv2
     e1 <- addEltTH endianness interps bv1
     e2 <- addEltTH endianness interps bv2
-    liftQ [| G.addExpr =<< join ((TR.bvconcat <$> $(refBinding e1) <*> $(refBinding e2) <*> pure $(natReprTH v) <*> pure $(natReprTH u) <*> pure $(natReprTH w))) |]
+    liftQ $ [| G.addExpr =<< $(joinOp2 [| \v1 v2 -> TR.bvconcat v1 v2 $(natReprTH v) $(natReprTH u) $(natReprTH w) |] e1 e2) |]
   S.BVSelect idx n bv -> do
     let w = S.bvWidth bv
     case natValue n + 1 <= natValue w of
       True -> do
         e <- addEltTH endianness interps bv
-        liftQ [| G.addExpr =<< join ((TR.bvselect <$> $(refBinding e) <*> pure $(natReprTH n) <*> pure $(natReprTH idx) <*> pure $(natReprTH w))) |]
+        liftQ [| G.addExpr =<< $(joinOp1 [| \v1 -> TR.bvselect v1 $(natReprTH n) $(natReprTH idx) $(natReprTH w) |] e) |]
       False -> do
         e <- addEltTH endianness interps bv
         liftQ [| case testEquality $(natReprTH n) $(natReprTH w) of
@@ -895,42 +909,43 @@ defaultAppEvaluator endianness elt interps = case elt of
                |]
   S.BVTestBit idx bv -> do
     bvValExp <- addEltTH endianness interps bv
-    liftQ [| addApp =<< (M.BVTestBit (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift (toInteger idx))) <$> $(refBinding bvValExp))
+    liftQ $ joinPure1 [| addApp |] [| M.BVTestBit (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift (toInteger idx))) |] bvValExp
-            |]
 
   S.SemiRingSum sm ->
     case WSum.sumRepr sm of
-      SR.SemiRingBVRepr SR.BVArithRepr w ->
+      SR.SemiRingBVRepr fl w ->
-        let smul mul e = do y <- addEltTH endianness interps e
+        let smul mul e = do
-                            letTH [| addApp =<< (M.BVMul $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) <$> $(refBinding y))
+              y <- addEltTH endianness interps e
-                                   |]
+              return $ [(y, BVS.asUnsigned mul)]
+            one = case fl of
+              SR.BVArithRepr -> 1
+              SR.BVBitsRepr -> SI.maxUnsigned w 
             sval v = do
-              EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
+              bnd <- EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
-            add x y = do
+              return $ [(bnd, one)]
-              letTH [| addApp =<< (M.BVAdd $(natReprTH w) <$> $(refBinding x) <*> $(refBinding y)) |]
+
-        in WSum.evalM add smul sval sm >>= extractBound
+        in do
-      SR.SemiRingBVRepr SR.BVBitsRepr w ->
+          bnds <- WSum.evalM (\a b -> return $ a ++ b) smul sval sm
-        let smul mul e = do y <- addEltTH endianness interps e
+          case all (\(bnd,_) -> isEager bnd) bnds of
-                            letTH [| addApp =<< (M.BVAnd $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) <$> $(refBinding y))
+            True -> do
-                                   |]
+              tms <- liftQ $ listE $ map (\(bnd, i) -> (tupE [refEager bnd, lift i])) bnds
-            sval v = do
+              liftQ [| sumBVs $(liftFlavor fl) $(natReprTH w) $(return tms) |]
-              EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
+            False -> do
-            add x y = do
+              tms <- liftQ $ listE $ map (\(bnd, i) -> (tupE [refBinding bnd, lift i])) bnds
-              letTH [| addApp =<< (M.BVXor $(natReprTH w) <$> $(refBinding x) <*> $(refBinding y)) |]
+              liftQ [| joinSumBVs $(liftFlavor fl) $(natReprTH w) $(return tms) |]
-        in WSum.evalM add smul sval sm >>= extractBound
       _ -> liftQ [| error "unsupported SemiRingSum repr for macaw semmc TH" |]
 
   S.SemiRingProd pd ->
     case WSum.prodRepr pd of
       SR.SemiRingBVRepr SR.BVArithRepr w ->
         let pmul x y = do
-              letTH [| addApp =<< (M.BVMul $(natReprTH w) <$> $(refBinding x) <*> $(refBinding y)) |]
+              bindPure2 [| addApp |] [| M.BVMul $(natReprTH w) |] x y
             unit = liftQ [| pure (M.BVValue $(natReprTH w) 1) |]
             convert = addEltTH endianness interps
         in WSum.prodEvalM pmul convert pd >>= maybe unit extractBound
       SR.SemiRingBVRepr SR.BVBitsRepr w ->
         let pmul x y = do
-              letTH [| addApp =<< (M.BVAnd $(natReprTH w) <$> $(refBinding x) <*> $(refBinding y)) |]
+              bindPure2 [| addApp |] [| M.BVAnd $(natReprTH w) |] x y
             unit = liftQ [| pure (M.BVValue $(natReprTH w) $(lift $ SI.maxUnsigned w)) |]
             convert = addEltTH endianness interps
         in WSum.prodEvalM pmul convert pd >>= maybe unit extractBound
@@ -942,70 +957,124 @@ defaultAppEvaluator endianness elt interps = case elt of
     -- These are all TH Exprs that are of the (Macaw) Value at run-time
     bs' <- mapM (addEltTH endianness interps) (S.bvOrToList bs)
     let por x y = do
-          letTH [| addApp =<< (M.BVOr $(natReprTH w) <$> $(refBinding x) <*> $(refBinding y)) |]
+          bindPure2 [| addApp |] [| M.BVOr $(natReprTH w) |] x y
     F.foldrM por (EagerBoundExp zero) bs' >>= extractBound
 
   S.BVShl w bv1 bv2 -> do
     e1 <- addEltTH endianness interps bv1
     e2 <- addEltTH endianness interps bv2
-    liftQ [| addApp =<< (M.BVShl $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2)) |]
+    liftQ $ joinPure2 [| addApp |] [| M.BVShl $(natReprTH w) |] e1 e2
   S.BVLshr w bv1 bv2 -> do
     e1 <- addEltTH endianness interps bv1
     e2 <- addEltTH endianness interps bv2
-    liftQ [| addApp =<< (M.BVShr $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2)) |]
+    liftQ $ joinPure2 [| addApp |] [| M.BVShr $(natReprTH w) |] e1 e2
   S.BVAshr w bv1 bv2 -> do
     e1 <- addEltTH endianness interps bv1
     e2 <- addEltTH endianness interps bv2
-    liftQ [| addApp =<< (M.BVSar $(natReprTH w) <$> $(refBinding e1) <*> $(refBinding e2)) |]
+    liftQ $ joinPure2 [| addApp |] [| M.BVSar $(natReprTH w) |] e1 e2
   S.BVZext w bv -> do
     e <- addEltTH endianness interps bv
-    liftQ [| addApp =<< (M.UExt <$> $(refBinding e) <*> pure $(natReprTH w)) |]
+    liftQ $ joinPure1 [| addApp |] [| (\x -> M.UExt x $(natReprTH w)) |] e
   S.BVSext w bv -> do
     e <- addEltTH endianness interps bv
-    liftQ [| addApp =<< (M.SExt <$> $(refBinding e) <*> pure $(natReprTH w)) |]
+    liftQ $ joinPure1 [| addApp |] [| (\x -> M.SExt x $(natReprTH w)) |] e
 
   _ -> error $ "unsupported Crucible elt: " <> show elt
 
 ----------------------------------------------------------------------
 
-data BoolMapOp = AndOp | OrOp
+getBVOps ::  1 SI.<= n
+         => CT.NatRepr n
+         -> SR.BVFlavorRepr t
+         -> (M.Value arch ids (M.BVType n)
+              -> M.Value arch ids (M.BVType n)
+              -> M.App (M.Value arch ids) (M.BVType n)
+            , M.Value arch ids (M.BVType n)
+              -> M.Value arch ids (M.BVType n)
+              -> M.App (M.Value arch ids) (M.BVType n))
+getBVOps repr fl = case fl of
+    SR.BVArithRepr -> (M.BVMul repr, M.BVAdd repr)
+    SR.BVBitsRepr -> (M.BVAnd repr, M.BVXor repr)
+
+liftFlavor :: SR.BVFlavorRepr t -> Q Exp
+liftFlavor fl = case fl of
+  SR.BVArithRepr -> [| SR.BVArithRepr |]
+  SR.BVBitsRepr -> [| SR.BVBitsRepr |]
+
+sumBVs :: 1 SI.<= n
+       => ( MSS.SimplifierExtension arch
+          , OrdF (M.ArchReg arch)
+          , M.MemWidth (M.RegAddrWidth (M.ArchReg arch))
+          , ShowF (M.ArchReg arch)
+          )
+       => SR.BVFlavorRepr t
+       -> CT.NatRepr n
+       -> [(M.Value arch ids (M.BVType n), Integer)]
+       -> G.Generator arch ids s (M.Value arch ids (M.BVType n))
+sumBVs fl repr vs = do
+  let (mulOp, addOp) = getBVOps repr fl
+  vals <- mapM (\(x,y) -> G.addExpr $ G.AppExpr $ mulOp x (M.BVValue repr y)) vs
+  foldM (\a b -> G.addExpr $ G.AppExpr $ addOp a b) (M.BVValue repr 0) vals
+
+joinSumBVs :: 1 SI.<= n
+           => ( MSS.SimplifierExtension arch
+              , OrdF (M.ArchReg arch)
+              , M.MemWidth (M.RegAddrWidth (M.ArchReg arch))
+              , ShowF (M.ArchReg arch)
+              )
+           => SR.BVFlavorRepr t
+           -> CT.NatRepr n
+           -> [(G.Generator arch ids s (M.Value arch ids (M.BVType n)), Integer)]
+           -> G.Generator arch ids s (M.Value arch ids (M.BVType n))
+joinSumBVs fl repr vs = do
+  let (mulOp, addOp) = getBVOps repr fl
+  vals <- mapM (\(xF,y) -> xF >>= \x -> G.addExpr $ G.AppExpr $ mulOp x (M.BVValue repr y)) vs
+  foldM (\a b -> G.addExpr $ G.AppExpr $ addOp a b) (M.BVValue repr 0) vals
 
 
-evalBoolMap :: A.Architecture arch
+allPreds :: ( MSS.SimplifierExtension arch
-            => M.Endianness
+            , OrdF (M.ArchReg arch)
-            -> BoundVarInterpretations arch t fs
+            , M.MemWidth (M.RegAddrWidth (M.ArchReg arch))
-            -> BoolMapOp
+            , ShowF (M.ArchReg arch)
-            -> Bool
+            )
+         => [(M.Value arch ids M.BoolType, Bool)]
+         -> G.Generator arch ids s (M.Value arch ids M.BoolType)
+allPreds vs = do
+  let
+    mkApp b (a, True) =  G.addExpr $ G.AppExpr $ M.AndApp a b
+    mkApp b (a, False) = do
+      notA <- G.addExpr $ G.AppExpr $ M.NotApp a
+      G.addExpr $ G.AppExpr $ M.AndApp notA b
+  foldM mkApp (M.BoolValue True) vs 
+
+joinPreds :: ( MSS.SimplifierExtension arch
+             , OrdF (M.ArchReg arch)
+             , M.MemWidth (M.RegAddrWidth (M.ArchReg arch))
+             , ShowF (M.ArchReg arch)
+             )
+          => [(G.Generator arch ids s (M.Value arch ids M.BoolType), Bool)]
+          -> G.Generator arch ids s (M.Value arch ids M.BoolType)
+joinPreds vs = do
+  let
+    mkApp b (aF, True) = do
+      a <- aF
+      G.addExpr $ G.AppExpr $ M.AndApp a b
+    mkApp b (aF, False) = do
+      a <- aF
+      notA <- G.addExpr $ G.AppExpr $ M.NotApp a
+      G.addExpr $ G.AppExpr $ M.AndApp notA b
+  foldM mkApp (M.BoolValue True) vs 
+
+
+
+boolMapList :: (forall tp. S.Expr t tp -> MacawQ arch t fs BoundExp)
             -> BooM.BoolMap (S.Expr t)
-            -> MacawQ arch t fs BoundExp
+            -> MacawQ arch t fs [(BoundExp, Bool)]
-evalBoolMap endianness interps op defVal bmap =
+boolMapList f bm = case BooM.viewBoolMap bm of
-  case BooM.viewBoolMap bmap of
+  BooM.BoolMapUnit -> return []
-    BooM.BoolMapUnit ->     letTH [| G.addExpr (boolBase $(lift defVal)) |]
+  BooM.BoolMapDualUnit -> do
-    BooM.BoolMapDualUnit -> letTH [| G.addExpr (bNotBase $(lift defVal)) |]
+    bnd <- EagerBoundExp <$> liftQ [| M.BoolValue False |]
-    BooM.BoolMapTerms ts ->
+    return $ [(bnd, True)]
-         do d <- letTH [| G.addExpr (boolBase $(lift defVal)) |]
+  BooM.BoolMapTerms ts -> liftM NE.toList $ forM ts $ \(e, p) -> do
-            F.foldl (joinBool endianness interps op) (return d) ts
+    eE <- f e
-
+    return $ (eE, p == BooM.Positive)
-
-boolBase, bNotBase :: A.Architecture arch => Bool -> G.Expr arch t 'M.BoolType
-boolBase = G.ValueExpr . M.BoolValue
-bNotBase = boolBase . not
-
-joinBool :: A.Architecture arch
-         => M.Endianness
-         -> BoundVarInterpretations arch t fs
-         -> BoolMapOp
-         -> MacawQ arch t fs BoundExp
-         -> (S.Expr t SI.BaseBoolType, S.Polarity)
-         -> MacawQ arch t fs BoundExp
-joinBool endianness interps op e r =
-  do n <- case r of
-            (t, BooM.Positive) -> do addEltTH endianness interps t
-            (t, BooM.Negative) -> do p <- addEltTH endianness interps t
-                                     letTH [| addApp =<< (M.NotApp <$> $(refBinding p)) |]
-     j <- e
-     case op of
-       AndOp ->
-         letTH [| addApp =<< (M.AndApp <$> $(refBinding j) <*> $(refBinding n)) |]
-       OrOp  ->
-         letTH [| addApp =<< (M.OrApp <$> $(refBinding j) <*> $(refBinding n)) |]

macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs

@@ -19,14 +19,27 @@ module Data.Macaw.SemMC.TH.Monad (
   letBindExpr,
   letBindPureExpr,
   bindTH,
+  letBindPat,
   letTH,
   extractBound,
   refBinding,
   inConditionalContext,
   isTopLevel,
-  definedFunction
+  definedFunction,
+  isEager,
+  refEager,
+  joinOp1,
+  joinOp2,
+  joinOp3,
+  joinPure1,
+  joinPure2,
+  joinPure3,
+  bindPure1,
+  bindPure2,
+  bindPure3
   ) where
 
+import           Control.Monad ( join )
 import qualified Control.Monad.Fail as MF
 import qualified Control.Monad.State.Strict as St
 import           Control.Monad.Trans ( lift )
@@ -37,6 +50,8 @@ import qualified Data.Sequence as Seq
 import           Language.Haskell.TH
 
 import qualified Data.Macaw.CFG as M
+import qualified Data.Parameterized.Context as Ctx
+import qualified Data.Parameterized.TraversableFC as FC
 import qualified Data.Parameterized.Map as Map
 import           Data.Parameterized.Some ( Some(..) )
 import qualified Lang.Crucible.Backend.Simple as S
@@ -85,6 +100,9 @@ data MacawTHConfig arch opc t fs =
                 -- ^ A TH action to generate the type tag for the architecture
                 , genLibraryFunction :: forall sym . Some (SF.FunctionFormula sym) -> Bool
                 , genOpcodeCase :: forall tps . opc tps -> Bool
+                , archTranslateType :: forall tp. Q Type -> Q Type -> SI.BaseTypeRepr tp -> Maybe (Q Type)
+                -- ^ An optional override when translating What4 types, where the first two
+                -- arguments correspond to the 'ids' and 's' type variables.
                 }
 
 data QState arch t fs = QState { accumulatedStatements :: !(Seq.Seq Stmt)
@@ -221,40 +239,54 @@ data BoundExp where
 -- and the new name is returned.
 bindExpr :: S.Expr t tp -> ExpQ -> MacawQ arch t fs BoundExp
 bindExpr elt eq = do
+  pureFn <- liftQ $ [| pure |]
   e <- liftQ eq
-  n <- liftQ (newName "val")
+  case e of
-  let res = VarE n
+    AppE f (VarE n) | pureFn == f -> return $ EagerBoundExp $ VarE n
-  St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> BindS (VarP n) e
+    _ -> do
-                       , expressionCache = M.insert (Some elt) res (expressionCache s)
+      n <- liftQ (newName "val")
-                       }
+      let res = VarE n
-  return (EagerBoundExp res)
+      St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> BindS (VarP n) e
+                           , expressionCache = M.insert (Some elt) res (expressionCache s)
+                           }
+      return (EagerBoundExp res)
 
 letBindPureExpr :: S.Expr t tp -> ExpQ -> MacawQ arch t fs BoundExp
 letBindPureExpr elt eq = do
   e <- liftQ eq
-  n <- liftQ (newName "lval")
+  case e of
-  let res = VarE n
+    VarE n -> return $ EagerBoundExp $ VarE n
-  St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD (VarP n) (NormalB e) []]
+    _ -> do
-                       , expressionCache = M.insert (Some elt) res (expressionCache s)
+      n <- liftQ (newName "lval")
-                       }
+      let res = VarE n
-  return (EagerBoundExp res)
+      St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD (VarP n) (NormalB e) []]
+                           , expressionCache = M.insert (Some elt) res (expressionCache s)
+                           }
+      return (EagerBoundExp res)
 
 letBindExpr :: S.Expr t tp -> Exp -> MacawQ arch t fs BoundExp
 letBindExpr elt e = do
-  n <- liftQ (newName "lval")
+  pureFn <- liftQ $ [| pure |]
-  let res = VarE n
+  case e of
-  St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD (VarP n) (NormalB e) []]
+    AppE f (VarE n) | pureFn == f -> return $ EagerBoundExp $ VarE n
-                       , lazyExpressionCache = M.insert (Some elt) res (lazyExpressionCache s)
+    _ -> do
-                       }
+      n <- liftQ (newName "lval")
-  return (LazyBoundExp res)
+      let res = VarE n
+      St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD (VarP n) (NormalB e) []]
+                           , lazyExpressionCache = M.insert (Some elt) res (lazyExpressionCache s)
+                           }
+      return (LazyBoundExp res)
 
 letTH :: ExpQ -> MacawQ arch t fs BoundExp
 letTH eq = do
   e <- liftQ eq
-  n <- liftQ (newName "lval")
+  case e of
-  St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD (VarP n) (NormalB e) []]
+    VarE n -> return $ LazyBoundExp $ VarE n
-                       }
+    _ -> do
-  return (LazyBoundExp (VarE n))
+     n <- liftQ (newName "lval")
+     St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD (VarP n) (NormalB e) []]
+                          }
+     return (LazyBoundExp (VarE n))
 
 bindTH :: ExpQ -> MacawQ arch t fs BoundExp
 bindTH eq = do
@@ -264,6 +296,14 @@ bindTH eq = do
                        }
   return (EagerBoundExp (VarE n))
 
+letBindPat :: S.Expr t tp -> (PatQ, ExpQ) -> ExpQ -> MacawQ arch t fs ()
+letBindPat elt (patq,resq) eq = do
+  pat <- liftQ patq
+  res <- liftQ resq
+  e <- liftQ eq
+  St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD pat (NormalB e) []]
+                       , expressionCache = M.insert (Some elt) res (expressionCache s) }
+
 definedFunction :: String -> MacawQ arch t fs (Maybe Exp)
 definedFunction name = do
   df <- St.gets definedFunctionEvaluator
@@ -286,3 +326,60 @@ refBinding be =
     EagerBoundExp e -> [| pure $(return e) |]
     -- If it is lazy, we need it "bare" in the applicative wrappers
     LazyBoundExp e -> return e
+
+isEager :: BoundExp -> Bool
+isEager be = case be of
+  EagerBoundExp _ -> True
+  LazyBoundExp _ -> False
+
+refEager :: BoundExp -> Q Exp
+refEager be = case be of
+  EagerBoundExp e -> return e
+  LazyBoundExp _ -> fail "refEager: cannot eagerly reference a lazy value"
+
+
+joinOp1 :: ExpQ -> BoundExp -> Q Exp
+joinOp1 fun arg1 = case isEager arg1 of
+  True -> [| $(fun) $(refEager arg1) |]
+  False -> [| $(fun) =<< $(refBinding arg1) |]
+
+joinOp2 :: ExpQ -> BoundExp -> BoundExp -> Q Exp
+joinOp2 fun arg1 arg2 = case all isEager [arg1, arg2] of
+  True -> [| $(fun) $(refEager arg1) $(refEager arg2) |]
+  False -> [| join ($(fun) <$> $(refBinding arg1) <*> $(refBinding arg2)) |]
+
+joinOp3 :: ExpQ -> BoundExp -> BoundExp -> BoundExp -> Q Exp
+joinOp3 fun arg1 arg2 arg3 = case all isEager [arg1, arg2, arg3] of
+  True -> [| $(fun) $(refEager arg1) $(refEager arg2) $(refEager arg3)|]
+  False -> [| join ($(fun) <$> $(refBinding arg1) <*> $(refBinding arg2) <*> $(refBinding arg3)) |]
+
+joinPure1 :: ExpQ -> ExpQ -> BoundExp -> Q Exp
+joinPure1 mfun fun arg1 = case isEager arg1 of
+  True -> [| $(mfun) ($(fun) $(refEager arg1)) |]
+  False -> [| $(mfun) =<< ($(fun) <$> $(refBinding arg1)) |]
+
+bindPure1 :: ExpQ -> ExpQ -> BoundExp -> MacawQ arch t fs BoundExp
+bindPure1 mfun fun arg1 = case isEager arg1 of
+  True -> bindTH $ joinPure1 mfun fun arg1
+  False -> letTH $ joinPure1 mfun fun arg1
+
+joinPure2 :: ExpQ -> ExpQ -> BoundExp -> BoundExp -> Q Exp
+joinPure2 mfun fun arg1 arg2 = case all isEager [arg1, arg2] of
+  True -> [| $(mfun) ($(fun) $(refEager arg1) $(refEager arg2)) |]
+  False -> [| $(mfun) =<< ($(fun) <$> $(refBinding arg1)) <*> $(refBinding arg2) |]
+
+bindPure2 :: ExpQ -> ExpQ -> BoundExp -> BoundExp -> MacawQ arch t fs BoundExp
+bindPure2 mfun fun arg1 arg2 = case all isEager [arg1, arg2] of
+  True -> bindTH $ joinPure2 mfun fun arg1 arg2
+  False -> letTH $ joinPure2 mfun fun arg1 arg2
+
+joinPure3 :: ExpQ -> ExpQ -> BoundExp -> BoundExp -> BoundExp -> Q Exp
+joinPure3 mfun fun arg1 arg2 arg3 = case all isEager [arg1, arg2, arg3] of
+  True -> [| $(mfun) ($(fun) $(refEager arg1) $(refEager arg2) $(refEager arg3)) |]
+  False -> [| $(mfun) =<< ($(fun) <$> $(refBinding arg1)) <*> $(refBinding arg2) <*> $(refBinding arg3) |]
+
+
+bindPure3 :: ExpQ -> ExpQ -> BoundExp -> BoundExp -> BoundExp -> MacawQ arch t fs BoundExp
+bindPure3 mfun fun arg1 arg2 arg3 = case all isEager [arg1, arg2, arg3] of
+  True -> bindTH $ joinPure3 mfun fun arg1 arg2 arg3
+  False -> letTH $ joinPure3 mfun fun arg1 arg2 arg3

refinement/src/Data/Macaw/Refinement/Solver.hs

@@ -28,7 +28,7 @@ data Solver = CVC4 | Yices | Z3
 
 withNewBackend :: (MonadIO m)
                => Solver
-               -> (forall proxy t solver fs sym . (sym ~ CBS.SimpleBackend t fs, CB.IsSymInterface sym, WPO.OnlineSolver t solver) => proxy solver -> WPF.ProblemFeatures -> sym -> m a)
+               -> (forall proxy t solver fs sym . (sym ~ CBS.SimpleBackend t fs, CB.IsSymInterface sym, WPO.OnlineSolver solver) => proxy solver -> WPF.ProblemFeatures -> sym -> m a)
                -> m a
 withNewBackend s k = do
   sym :: CBS.SimpleBackend PN.GlobalNonceGenerator (WE.Flags WE.FloatUninterpreted)
@@ -40,7 +40,7 @@ withNewBackend s k = do
       let features = WPF.useBitvectors .|. WPF.useSymbolicArrays .|. WPF.useStructs .|. WPF.useNonlinearArithmetic
       k proxy features sym
     Yices -> do
-      let proxy = Proxy @(WSY.Connection PN.GlobalNonceGenerator)
+      let proxy = Proxy @WSY.Connection
       liftIO $ WC.extendConfig WSY.yicesOptions (WI.getConfiguration sym)
       -- For some reason, non-linear arithmetic is required for cvc4 and z3 but doesn't work at all with yices
       let features = WPF.useBitvectors .|. WPF.useSymbolicArrays .|. WPF.useStructs .|. WPF.useLinearArithmetic

refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs

@@ -387,7 +387,7 @@ genIPConstraint ctx sym ipVal = liftIO $ do
 -- | Probe the SMT solver for additional models of the given expression up to a maximum @count@
 genModels
   :: forall t solver fs m arch sym w proxy
-   . ( W.OnlineSolver t solver
+   . ( W.OnlineSolver solver
      , KnownNat w
      , 1 <= w
      , MonadIO m
@@ -417,7 +417,7 @@ genModels proxy sym solver_proc assumptions expr count
 
 extractIPModels :: forall arch solver m sym t fp
                  . ( MS.SymArchConstraints arch
-                   , W.OnlineSolver t solver
+                   , W.OnlineSolver solver
                    , MU.MonadUnliftIO m
                    , CB.IsSymInterface sym
                    , sym ~ CBS.SimpleBackend t fp