From 5b93b1fa002ddd39e07d9ed8a1c0ede6c5730791 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Thu, 16 Jul 2020 23:08:58 -0700
Subject: [PATCH 01/20] [macaw-semmc] updates for app-refactor what4 changes

See https://github.com/GaloisInc/what4/pull/55
---
 macaw-semmc/src/Data/Macaw/SemMC/TH.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
index b9eebeff..7695dc40 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
@@ -655,7 +655,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 +666,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))

From f695c4d4c1757aac553c4462e1f6825031e2f8f2 Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Fri, 17 Jul 2020 17:30:44 -0700
Subject: [PATCH 02/20] [macaw-refinement] updates for app-refactor what4
 changes.

---
 refinement/src/Data/Macaw/Refinement/Solver.hs            | 4 ++--
 refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/refinement/src/Data/Macaw/Refinement/Solver.hs b/refinement/src/Data/Macaw/Refinement/Solver.hs
index f7383af0..ddd9cb25 100644
--- a/refinement/src/Data/Macaw/Refinement/Solver.hs
+++ b/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
diff --git a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs b/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
index ee473693..e1389108 100644
--- a/refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+++ b/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

From 0cb0a89748c70cd6cf7186326e5983a9c4ff1e0e Mon Sep 17 00:00:00 2001
From: Kevin Quick <kquick@galois.com>
Date: Mon, 20 Jul 2020 14:18:35 -0700
Subject: [PATCH 03/20] Update submodules.

---
 deps/crucible        | 2 +-
 deps/elf-edit        | 2 +-
 deps/flexdis86       | 2 +-
 deps/semmc           | 2 +-
 deps/what4           | 2 +-
 deps/what4-serialize | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index a4999579..5cb47b4f 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit a4999579844590f971717b4082cb7697626de047
+Subproject commit 5cb47b4f77299b54b0ead3f93f25dc24447c80f3
diff --git a/deps/elf-edit b/deps/elf-edit
index 31a4d5a3..3a596093 160000
--- a/deps/elf-edit
+++ b/deps/elf-edit
@@ -1 +1 @@
-Subproject commit 31a4d5a3a871b16c0f9cb5e488f5cca2e5f4fd86
+Subproject commit 3a596093c264d0aa4c8666ea408c3ca67caf7ebe
diff --git a/deps/flexdis86 b/deps/flexdis86
index 5981054d..51317819 160000
--- a/deps/flexdis86
+++ b/deps/flexdis86
@@ -1 +1 @@
-Subproject commit 5981054db6354e0deb54323d93274d66e6a119f9
+Subproject commit 51317819dbb7a39891f36010d3c4bf196789d032
diff --git a/deps/semmc b/deps/semmc
index 72f50435..6506a5d2 160000
--- a/deps/semmc
+++ b/deps/semmc
@@ -1 +1 @@
-Subproject commit 72f504352a36fb8f6067c2d58979114f128cbb54
+Subproject commit 6506a5d2c68fdbc8d3a9f64c841e08754d1aecc0
diff --git a/deps/what4 b/deps/what4
index 72d105fd..f9a8f950 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit 72d105fd4e9c08c3f41bf69db7273e7d1fcdb93a
+Subproject commit f9a8f950e7c66f0f04312ce3983a42f3facd576e
diff --git a/deps/what4-serialize b/deps/what4-serialize
index 140ad099..e0a013a2 160000
--- a/deps/what4-serialize
+++ b/deps/what4-serialize
@@ -1 +1 @@
-Subproject commit 140ad099d7856c35d03ee8f18a94af00867b8eff
+Subproject commit e0a013a24a459a71f96a2238a238ff4f3bc9f111

From 547796118d804bb299dea82281ad31e63357a459 Mon Sep 17 00:00:00 2001
From: Sam Breese <chameco@users.noreply.github.com>
Date: Tue, 14 Jul 2020 14:41:16 -0400
Subject: [PATCH 04/20] x86: Add semantics for some AVX2 instructions (#149)

* x86: Add semantics for the vpsrld and vpsrlq instructions

* x86: Add semantics for vpaddq

* Fix Haddock for PointwiseLogicalShiftR

* x86: Change vpsubd to PtSub rather than PtAdd
---
 x86/src/Data/Macaw/X86.hs                   |  1 +
 x86/src/Data/Macaw/X86/ArchTypes.hs         | 23 +++++++++++++++++++++
 x86/src/Data/Macaw/X86/Semantics/AVX.hs     | 21 ++++++++++++++++++-
 x86_symbolic/src/Data/Macaw/X86/Crucible.hs | 13 ++++++++++++
 4 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/x86/src/Data/Macaw/X86.hs b/x86/src/Data/Macaw/X86.hs
index d276f3d1..528fdc22 100644
--- a/x86/src/Data/Macaw/X86.hs
+++ b/x86/src/Data/Macaw/X86.hs
@@ -381,6 +381,7 @@ transferAbsValue r f =
     VOp2 {} -> TopV
     Pointwise2 {} -> TopV
     PointwiseShiftL {} -> TopV
+    PointwiseLogicalShiftR {} -> TopV
     VExtractF128 {} -> TopV
     VInsert {} -> TopV
 
diff --git a/x86/src/Data/Macaw/X86/ArchTypes.hs b/x86/src/Data/Macaw/X86/ArchTypes.hs
index 3e6e3fc1..ddbafe55 100644
--- a/x86/src/Data/Macaw/X86/ArchTypes.hs
+++ b/x86/src/Data/Macaw/X86/ArchTypes.hs
@@ -662,6 +662,24 @@ data X86PrimFn f tp where
                   -> !(f (BVType sz))
                   -> X86PrimFn f (BVType (elNum * elSize))
 
+  -- | Shift right each element in the vector by the given amount.
+  -- The new ("shifted-in") bits are 0.
+  --
+  -- For the expression @PointwiseShiftLogicalR n w amtw vec amt@:
+  --
+  -- * @n@ is the number of elements in the vector
+  -- * @w@ is the size of each element in bits
+  -- * @amtw@ is the size of the shift amount in bits
+  -- * @vec@ is the vector to be inserted into
+  -- * @amt@ is the shift amount in bits
+  PointwiseLogicalShiftR :: (1 <= elSize, 1 <= elNum, 1 <= sz) =>
+                            !(NatRepr elNum)
+                         -> !(NatRepr elSize)
+                         -> !(NatRepr sz)
+                         -> !(f (BVType (elNum * elSize)))
+                         -> !(f (BVType sz))
+                         -> X86PrimFn f (BVType (elNum * elSize))
+
   -- | Pointwise binary operation on vectors. Should not have side effects.
   --
   -- For the expression @Pointwise2 n w op vec1 vec2@:
@@ -723,6 +741,7 @@ instance HasRepr (X86PrimFn f) TypeRepr where
       X87_FMul{} -> knownRepr
       X87_FST tp _ -> FloatTypeRepr (typeRepr tp)
       PointwiseShiftL n w _ _ _ -> packedAVX n w
+      PointwiseLogicalShiftR n w _ _ _ -> packedAVX n w
       VInsert n w _ _ _ -> packedAVX n w
       VOp1 w _ _ -> BVTypeRepr w
       VOp2 w _ _ _ -> BVTypeRepr w
@@ -779,6 +798,7 @@ instance TraversableFC X86PrimFn where
       VOp1 w o x   -> VOp1 w o <$> go x
       VOp2 w o x y -> VOp2 w o <$> go x <*> go y
       PointwiseShiftL e n s x y -> PointwiseShiftL e n s <$> go x <*> go y
+      PointwiseLogicalShiftR e n s x y -> PointwiseLogicalShiftR e n s <$> go x <*> go y
       Pointwise2 n w o x y -> Pointwise2 n w o <$> go x <*> go y
       VExtractF128 x i -> (`VExtractF128` i) <$> go x
       VInsert n w v e i -> (\v' e' -> VInsert n w v' e' i) <$> go v <*> go e
@@ -831,6 +851,8 @@ instance IsArchFn X86PrimFn where
       VOp2 _ o x y -> sexprA (show o) [ pp x, pp y ]
       PointwiseShiftL _ w _ x y -> sexprA "pointwiseShiftL"
                                      [ ppShow (widthVal w), pp x, pp y ]
+      PointwiseLogicalShiftR _ w _ x y -> sexprA "pointwiseLogicalShiftR"
+                                            [ ppShow (widthVal w), pp x, pp y ]
       Pointwise2 _ w o x y -> sexprA (show o)
                                 [ ppShow (widthVal w) , pp x , pp y ]
       VExtractF128 x i -> sexprA "vextractf128" [ pp x, ppShow i ]
@@ -882,6 +904,7 @@ x86PrimFnHasSideEffects f =
     VOp1 {} -> False
     VOp2 {} -> False
     PointwiseShiftL {} -> False
+    PointwiseLogicalShiftR {} -> False
     Pointwise2 {} -> False
     VExtractF128 {} -> False
     VInsert {} -> False
diff --git a/x86/src/Data/Macaw/X86/Semantics/AVX.hs b/x86/src/Data/Macaw/X86/Semantics/AVX.hs
index f78df92c..23d8ba75 100644
--- a/x86/src/Data/Macaw/X86/Semantics/AVX.hs
+++ b/x86/src/Data/Macaw/X86/Semantics/AVX.hs
@@ -143,6 +143,20 @@ avxPointwiseShiftL mnem sz =
                   arg1 <~ PointwiseShiftL elN sz amtw v a
              _ -> fail ("[" ++ mnem ++ "]: invalid arguments")
 
+avxPointwiseLogicalShiftR :: (1 <= n) => String -> NatRepr n -> InstructionDef
+avxPointwiseLogicalShiftR mnem sz =
+  avx3 mnem $ \arg1 arg2 arg3 ->
+      do SomeBV vec <- getSomeBVValue arg2
+         SomeBV amt <- getSomeBVValue arg3
+         let vw   = typeWidth vec
+             amtw = typeWidth amt
+         withDivModNat vw sz $ \elN remi ->
+           case (testEquality remi n0, testLeq n1 elN) of
+             (Just Refl, Just LeqProof) ->
+               do v <- eval vec
+                  a <- eval amt
+                  arg1 <~ PointwiseLogicalShiftR elN sz amtw v a
+             _ -> fail ("[" ++ mnem ++ "]: invalid arguments")
 
 avxInsert :: String -> InstructionDef
 avxInsert mnem =
@@ -197,12 +211,17 @@ all_instructions =
   , avxPointwiseShiftL "vpslld" n32
   , avxPointwiseShiftL "vpsllq" n64
 
+  , avxPointwiseLogicalShiftR "vpsrld" n32
+  , avxPointwiseLogicalShiftR "vpsrlq" n64
+
   , avxOp1I "vpslldq" VShiftL
   , avxOp1I "vpsrldq" VShiftR
   , avxOp1I "vpshufd" VShufD
 
   , avxPointwise2 "vpaddd" PtAdd n32
-  , avxPointwise2 "vpsubd" PtAdd n32
+  , avxPointwise2 "vpaddq" PtAdd n64
+
+  , avxPointwise2 "vpsubd" PtSub n32
 
   , avxOp2 "vpand" VPAnd
   , avxOp2 "vpor" VPOr
diff --git a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
index c6c6fd81..fb2cce7b 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Crucible.hs
@@ -414,6 +414,11 @@ pureSem sym fn = do
          vecOp1 sym LittleEndian (natMultiply elNum elSz) elSz bits $ \xs ->
               fmap (\x -> bvShiftL elSz shSz x amt') xs
 
+    M.PointwiseLogicalShiftR elNum elSz shSz bits amt ->
+      do amt' <- getBitVal (symIface sym) amt
+         vecOp1 sym LittleEndian (natMultiply elNum elSz) elSz bits $ \xs ->
+              fmap (\x -> bvLogicalShiftR elSz shSz x amt') xs
+
     M.Pointwise2 elNum elSz op v1 v2 ->
       vecOp2 sym LittleEndian (natMultiply elNum elSz) elSz v1 v2 $ \xs ys ->
         V.zipWith (semPointwise op elSz) xs ys
@@ -791,6 +796,14 @@ bvShiftL w i vw vi = app (BVShl w vw amt)
                 NatCaseLT LeqProof -> app (BVZext w i vi)
                 NatCaseGT LeqProof -> app (BVTrunc w i vi)
 
+bvLogicalShiftR :: (1 <= w, 1 <= i) =>
+  NatRepr w -> NatRepr i ->
+  E sym (BVType w) -> E sym (BVType i) -> E sym (BVType w)
+bvLogicalShiftR w i vw vi = app (BVLshr w vw amt)
+  where amt = case testNatCases i w of
+                NatCaseEQ -> vi
+                NatCaseLT LeqProof -> app (BVZext w i vi)
+                NatCaseGT LeqProof -> app (BVTrunc w i vi)
 
 
 --------------------------------------------------------------------------------

From 62dd08f5a1267a13c3b9993c5c7e3c962f2cb5e6 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 16:16:29 -0700
Subject: [PATCH 05/20] add more cases for simplifying boolean Muxes

---
 macaw-aarch32/src/Data/Macaw/ARM/Simplify.hs | 21 +++++++++++++++++++-
 macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs |  2 ++
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Simplify.hs b/macaw-aarch32/src/Data/Macaw/ARM/Simplify.hs
index 15e97b32..6c5266a9 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Simplify.hs
+++ b/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?
diff --git a/macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs b/macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs
index 1fff4dbe..f7666f42 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/Simplify.hs
+++ b/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)

From 98a429b7e0cfac07aaa19817d244e86f96873eea Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 16:32:34 -0700
Subject: [PATCH 06/20] avoid using applicative binds for eager values

---
 .../Data/Macaw/ARM/Semantics/ARMSemantics.hs  |  3 +
 .../src/Data/Macaw/ARM/Semantics/TH.hs        | 20 +++--
 macaw-semmc/src/Data/Macaw/SemMC/TH.hs        | 76 +++++++++----------
 macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs  | 73 +++++++++++++++++-
 4 files changed, 124 insertions(+), 48 deletions(-)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs
index 0e3857ac..7c47f918 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs
+++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs
@@ -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,8 @@ execInstruction =
                                   , archTypeQ = [t| ARMSem.AArch32 |]
                                   , genLibraryFunction = notVecLib
                                   , genOpcodeCase = notVecOpc
+                                  , getExprFields = Just $ getFlds
+                                  , archTranslateType = armTranslateType
                                   }
 
        genExecInstruction (Proxy @ARMSem.AArch32)
diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
index cda18187..6e7c508c 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
+++ b/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,9 @@ module Data.Macaw.ARM.Semantics.TH
     , getSIMD
     , setSIMD
     , loadSemantics
+    , armGetFields
+    , armTranslateType
+    , FieldGetter(..)
     )
     where
 
@@ -27,12 +33,13 @@ 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
@@ -78,7 +85,7 @@ armNonceAppEval bvi nonceApp =
                 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 +93,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 +101,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 +109,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,11 +120,10 @@ 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
diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
index 7695dc40..102010b9 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
@@ -616,7 +616,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) |]
@@ -726,10 +729,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) |]
-          -- FIXME: Check if all argExprs are 'EagerBoundExp's; if so, generate
-          -- a pure let bound version instead
-          liftQ [| join $(foldl applyQ [| return $(return fun) |] argExprs) |]
+          case all isEager argExprs of
+            True -> liftQ $ foldl appE (return fun) (map refEager argExprs)
+            False -> do
+              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 +838,19 @@ 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.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 =<<
-                                   (M.Mux M.BoolTypeRepr <$>
-                                    $(refBinding testE) <*> $(refBinding tE) <*> $(refBinding 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.BaseBoolRepr -> liftQ $ joinPure3 [| addApp |] [| M.Mux M.BoolTypeRepr |] testE tE fE
+      CT.BaseBVRepr w -> liftQ $ joinPure3 [| addApp |] [| M.Mux (M.BVTypeRepr $(natReprTH w)) |] testE tE fE
+      CT.BaseFloatRepr fpp -> liftQ $ joinPure3 [| addApp |] [| M.Mux (M.FloatTypeRepr $(floatInfoFromPrecisionTH fpp)) |] testE tE 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 +862,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,28 +891,28 @@ 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 ->
-        let smul mul e = do y <- addEltTH endianness interps e
-                            letTH [| addApp =<< (M.BVMul $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) <$> $(refBinding y))
-                                   |]
+        let smul mul e = do
+              y <- addEltTH endianness interps e
+              bindPure1 [| addApp |] [| M.BVMul $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) |] y
+
             sval v = do
               EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
             add x y = do
-              letTH [| addApp =<< (M.BVAdd $(natReprTH w) <$> $(refBinding x) <*> $(refBinding y)) |]
+              bindPure2 [| addApp |] [| M.BVAdd $(natReprTH w) |] x y
         in WSum.evalM add smul sval sm >>= extractBound
       SR.SemiRingBVRepr SR.BVBitsRepr w ->
         let smul mul e = do y <- addEltTH endianness interps e
-                            letTH [| addApp =<< (M.BVAnd $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) <$> $(refBinding y))
-                                   |]
+                            bindPure1 [| addApp |] [| M.BVAnd $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) |] y
+
             sval v = do
               EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
             add x y = do
-              letTH [| addApp =<< (M.BVXor $(natReprTH w) <$> $(refBinding x) <*> $(refBinding y)) |]
+              bindPure2 [| addApp |] [| M.BVXor $(natReprTH w) |] x y
         in WSum.evalM add smul sval sm >>= extractBound
       _ -> liftQ [| error "unsupported SemiRingSum repr for macaw semmc TH" |]
 
@@ -924,13 +920,13 @@ defaultAppEvaluator endianness elt interps = case elt of
     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,27 +938,27 @@ 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
 
diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
index 7fc871ba..f23dd56d 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
@@ -24,9 +24,21 @@ module Data.Macaw.SemMC.TH.Monad (
   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 +49,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
@@ -286,3 +300,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

From dcd5339b5a40d03752de6b48ed6deac5995fa94f Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 16:39:41 -0700
Subject: [PATCH 07/20] allow for manual bind pattern

---
 macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
index f23dd56d..980b8164 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
@@ -19,6 +19,7 @@ module Data.Macaw.SemMC.TH.Monad (
   letBindExpr,
   letBindPureExpr,
   bindTH,
+  letBindPat,
   letTH,
   extractBound,
   refBinding,
@@ -278,6 +279,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

From 3e03ec11ab96b3988600965d306052dcb582d099 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 17:39:22 -0700
Subject: [PATCH 08/20] allow for arch-specific type translation

---
 macaw-semmc/src/Data/Macaw/SemMC/TH.hs       | 21 +++++++++++++-------
 macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs |  3 +++
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
index 102010b9..0d1cd774 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
@@ -568,11 +568,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 =
-        [t| M.Value $(archTypeQ thConf) $(idsTy) $(translateBaseType tp) |]
+      translate tp = case archTranslateType thConf idsTy sTy tp of
+        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)
-                     $(translate (ffRetType ff)) |]
+      retHsTy = [t| G.Generator $(archTypeQ thConf) $(idsTy) $(sTy) $(translate (ffRetType ff)) |]
       ty = foldr (\a r -> [t| $(a) -> $(r) |]) retHsTy argHsTys
       body = doE (map return stmts)
   sig <- sigD var ty
@@ -580,10 +581,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.BaseBVRepr n -> appT [t| M.BVType |] (litT (numTyLit (intValue n)))
+    CT.BaseBoolRepr -> [| M.BoolTypeRepr |]
+    CT.BaseBVRepr n -> [| M.BVTypeRepr $(natReprTH n) |]
     _ -> fail $ "unsupported base type: " ++ show tp
 
 -- | wrapper around bitvector constants that forces some type
diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
index 980b8164..3ebf7a39 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
@@ -100,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)

From 838ef3924d5a137f831329fdd88d23cc503a4231 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 17:46:14 -0700
Subject: [PATCH 09/20] aarch32: wrap up stateful operations as values

---
 .../src/Data/Macaw/ARM/Semantics/TH.hs        | 362 ++++++++++--------
 1 file changed, 196 insertions(+), 166 deletions(-)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
index 6e7c508c..5593cc61 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
+++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
@@ -79,6 +79,29 @@ 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
@@ -331,77 +354,41 @@ armNonceAppEval bvi nonceApp =
                   op4e <- addEltTH M.LittleEndian bvi op4
                   liftQ [| G.addExpr =<< (FPRoundInt knownNat <$> $(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
-          -- being ambiguous, which is an error for various reasons.
-          --
-          -- 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)) |]
+          "uf_init_gprs" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteGPRs) |]
+          "uf_init_memory" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteMemory)|]
+          "uf_init_simds" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteSIMDs) |]
 
 
-          -- NOTE: These cases are tricky because they generate groups of
-          -- statements that need to behave a bit differently in (eager)
-          -- 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.
+          -- These functions indicate that the wrapped monadic actions in the corresponding
+          -- 'ARMWriteAction' should be executed, committing their stateful actions.
           "uf_update_gprs"
             | Ctx.Empty Ctx.:> gprs <- args -> Just $ do
-              istl <- isTopLevel
-              case istl of
-                False -> do
-                  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'
+                gprs' <- addEltTH M.LittleEndian bvi gprs
+                appendStmt $ [| join (execWriteAction <$> $(refBinding gprs')) |]
+                liftQ [| return $ M.BoolValue True |]
+                  
           "uf_update_simds"
             | Ctx.Empty Ctx.:> simds <- args -> Just $ do
-                istl <- isTopLevel
-                case istl of
-                  False -> do
-                    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'
+                simds' <- addEltTH M.LittleEndian bvi simds
+                appendStmt $ [| join (execWriteAction <$> $(refBinding simds')) |]
+                appendStmt [| setWriteMode WriteNone |]
+                liftQ [| return $ M.BoolValue True |]
+
           "uf_update_memory"
             | Ctx.Empty Ctx.:> mem <- args -> Just $ do
-                istl <- isTopLevel
-                case istl of
-                  False -> do
-                    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'
+                mem' <- addEltTH M.LittleEndian bvi mem
+                appendStmt $ [| join (execWriteAction <$> $(refBinding mem')) |]
+                liftQ [| return $ M.BoolValue True |]
 
+          "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 $ M.BoolValue True |]
           _ | "uf_assertBV_" `isPrefixOf` fnName ->
             case args of
               Ctx.Empty Ctx.:> assert Ctx.:> bv -> Just $ do
@@ -417,15 +404,33 @@ 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
 
 natReprFromIntTH :: Int -> Q Exp
 natReprFromIntTH i = [| knownNat :: M.NatRepr $(litT (numTyLit (fromIntegral i))) |]
 
+
+data ARMWriteActionK =
+    ARMWriteGPRsK
+  | ARMWriteMemoryK
+  | ARMWriteSIMDsK
+
+data ARMWriteActionRepr (tp :: ARMWriteActionK) where
+  ARMWriteGPRs :: ARMWriteActionRepr 'ARMWriteGPRsK
+  ARMWriteMemory :: ARMWriteActionRepr 'ARMWriteMemoryK
+  ARMWriteSIMDs :: ARMWriteActionRepr 'ARMWriteSIMDsK
+
+newtype ARMWriteAction ids s tp where
+  ARMWriteAction :: G.Generator ARM.AArch32 ids s tp -> ARMWriteAction ids s tp
+  deriving (Functor, Applicative, Monad)
+
+execWriteAction :: ARMWriteAction ids s tp -> G.Generator ARM.AArch32 ids s tp
+execWriteAction (ARMWriteAction f) = f
+
 data WriteMode =
   WriteNone
   | WriteGPRs
@@ -433,55 +438,31 @@ data WriteMode =
   | WriteMemory
   deriving (Show, Eq, Lift)
 
-getWriteMode :: G.Generator ARM.AArch32 ids s WriteMode
-getWriteMode = do
-  G.getRegVal ARMWriteMode >>= \case
-      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 ()
-setWriteMode wm =
-  let
-    i = case wm of
-      WriteNone -> 0
-      WriteGPRs -> 1
-      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 (ARMWriteActionRepr 'ARMWriteMemoryK)
          -> 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)
-writeMem mem addr sz val = do
-  wm <- getWriteMode
-  case wm of
-    WriteMemory -> do
-      G.addStmt (M.WriteMem addr (M.BVMemRepr sz M.LittleEndian) val)
-      return mem
-    _ -> return mem
+         -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteMemoryK))
+writeMem sz mem addr val = return $ do
+  _ <- mem
+  ARMWriteAction $ G.addStmt (M.WriteMem addr (M.BVMemRepr sz M.LittleEndian) val)
+  return $ ARMWriteMemory
 
-setGPR :: M.Value ARM.AArch32 ids tp
+setGPR :: ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteGPRsK)
        -> 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 (ARMWriteActionRepr 'ARMWriteGPRsK))
 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
-    WriteGPRs -> G.setRegVal reg v
-    _ -> return ()
-  return handle
+  return $ do
+    _ <- handle
+    ARMWriteAction $ G.setRegVal reg v
+    return $ ARMWriteGPRs
 
 getGPR :: M.Value ARM.AArch32 ids tp
        -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids (M.BVType 32))
@@ -493,20 +474,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
-       -> M.Value ARM.AArch32 ids (M.BVType 8)
-       -> M.Value ARM.AArch32 ids (M.BVType 128)
-       -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids tp)
+setSIMD :: ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteSIMDsK)
+        -> M.Value ARM.AArch32 ids (M.BVType 8)
+        -> M.Value ARM.AArch32 ids (M.BVType 128)
+        -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteSIMDsK))
 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
-    WriteSIMDs -> G.setRegVal reg v
-    _ -> return ()
-  return handle
+  return $ do
+    _ <- handle
+    ARMWriteAction $ G.setRegVal reg v
+    return $ ARMWriteSIMDs
+
 
 getSIMD :: M.Value ARM.AArch32 ids tp
        -> G.Generator ARM.AArch32 ids s (M.Value ARM.AArch32 ids (M.BVType 128))
@@ -516,13 +498,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
-
-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
-
+  G.getRegSnapshotVal reg
 
 -- ----------------------------------------------------------------------
 
@@ -542,33 +518,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
---
--- Many conditionals in the semantics are translated as muxes (effectively
--- 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
--- side effects to happen if the condition really is true.
---
--- This combinator checks to see if the condition is concretely true or false
--- (as expected) and then evaluates the corresponding 'G.Generator' action.
---
--- 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
+-- | 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
+-- we can translate it into a haskell if-then-else.
+
+concreteIte :: M.Value ARM.AArch32 ids (M.BoolType)
+            -> a
+            -> a
+            -> a
+concreteIte 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
 --
@@ -589,6 +549,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) (ARMWriteActionRepr 'ARMWriteMemoryK) |]
+      _ | Just Refl <- testEquality tp' (knownRepr :: WT.BaseTypeRepr ASL.AllSIMDBaseType) ->
+          [t| ARMWriteAction $(idsTy) $(sTy) (ARMWriteActionRepr 'ARMWriteSIMDsK) |]
+      _ | Just Refl <- testEquality tp' (knownRepr :: WT.BaseTypeRepr ASL.AllGPRBaseType) ->
+          [t| ARMWriteAction $(idsTy) $(sTy) (ARMWriteActionRepr 'ARMWriteGPRsK) |]
+      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
@@ -596,41 +607,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
-        -- conditionals that are guarding the state update functions with
-        -- mutation.
-        --
-        -- We need to ensure that state updates are only done lazily.  This
-        -- 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.
+        -- In this case, the placeholder type indicates that
+        -- expression is to be translated as a (wrapped) stateful action
+        -- rather than an actual macaw term. This is therefore translated
+        -- as a Haskell if-then-else statement, rather than
+        -- a Mux.
         testE <- addEltTH endianness interps test
-        inConditionalContext $ do
-          tE <- addEltTH endianness interps t
-          fE <- addEltTH endianness interps f
-          liftQ [| join (concreteIte PC.knownRepr <$> $(refBinding testE) <*> (return $(refBinding tE)) <*> (return $(refBinding fE))) |]
+        tE <- addEltTH endianness interps t
+        fE <- addEltTH endianness interps f
+        case all isEager [testE, tE, fE] of
+          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.:> _)) <- WT.exprType struct -> Just $ do
+        structE <- addEltTH endianness interps struct
+        extractBound structE
+      WB.StructField struct idx _ -> Just $ do
+        WT.BaseStructRepr reprs <- return $ WT.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 ->

From 468c329fa163792f062383c7ca71e2de8e4eba04 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 17:41:31 -0700
Subject: [PATCH 10/20] use compilation-friendly boolean and bitvector ops

---
 macaw-semmc/src/Data/Macaw/SemMC/TH.hs | 151 ++++++++++++++++++++++---
 1 file changed, 133 insertions(+), 18 deletions(-)

diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
index 0d1cd774..f040beee 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
@@ -36,18 +36,24 @@ module Data.Macaw.SemMC.TH (
   floatInfoTH,
   floatInfoFromPrecisionTH,
   symFnName,
-  asName
+  asName,
+  translateBaseType,
+  translateBaseTypeRepr,
+  sequenceAFC,
+  AppFC(..),
+  execAppFC
   ) 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(..) )
@@ -846,7 +852,15 @@ defaultAppEvaluator endianness elt interps = case elt of
   S.NotPred bool -> do
     e <- addEltTH endianness interps bool
     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
@@ -902,25 +916,26 @@ defaultAppEvaluator endianness elt interps = case elt of
 
   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
-              bindPure1 [| addApp |] [| M.BVMul $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) |] y
-
+              return $ [(y, BVS.asUnsigned mul)]
+            one = case fl of
+              SR.BVArithRepr -> 1
+              SR.BVBitsRepr -> WT.maxUnsigned w 
             sval v = do
-              EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
-            add x y = do
-              bindPure2 [| addApp |] [| M.BVAdd $(natReprTH w) |] x y
-        in WSum.evalM add smul sval sm >>= extractBound
-      SR.SemiRingBVRepr SR.BVBitsRepr w ->
-        let smul mul e = do y <- addEltTH endianness interps e
-                            bindPure1 [| addApp |] [| M.BVAnd $(natReprTH w) (M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned mul))) |] y
+              bnd <- EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
+              return $ [(bnd, one)]
 
-            sval v = do
-              EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
-            add x y = do
-              bindPure2 [| addApp |] [| M.BVXor $(natReprTH w) |] x y
-        in WSum.evalM add smul sval sm >>= extractBound
+        in do
+          bnds <- WSum.evalM (\a b -> return $ a ++ b) smul sval sm
+          case all (\(bnd,_) -> isEager bnd) bnds of
+            True -> do
+              tms <- liftQ $ listE $ map (\(bnd, i) -> (tupE [refEager bnd, lift i])) bnds
+              liftQ [| sumBVs $(liftFlavor fl) $(natReprTH w) $(return tms) |]
+            False -> do
+              tms <- liftQ $ listE $ map (\(bnd, i) -> (tupE [refBinding bnd, lift i])) bnds
+              liftQ [| joinSumBVs $(liftFlavor fl) $(natReprTH w) $(return tms) |]
       _ -> liftQ [| error "unsupported SemiRingSum repr for macaw semmc TH" |]
 
   S.SemiRingProd pd ->
@@ -1012,3 +1027,103 @@ joinBool endianness interps op e r =
          letTH [| addApp =<< (M.AndApp <$> $(refBinding j) <*> $(refBinding n)) |]
        OrOp  ->
          letTH [| addApp =<< (M.OrApp <$> $(refBinding j) <*> $(refBinding n)) |]
+
+
+
+
+
+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
+
+
+allPreds :: ( MSS.SimplifierExtension arch
+            , OrdF (M.ArchReg arch)
+            , M.MemWidth (M.RegAddrWidth (M.ArchReg arch))
+            , ShowF (M.ArchReg arch)
+            )
+         => [(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, Bool)]
+boolMapList f bm = case BooM.viewBoolMap bm of
+  BooM.BoolMapUnit -> return []
+  BooM.BoolMapDualUnit -> do
+    bnd <- EagerBoundExp <$> liftQ [| M.BoolValue False |]
+    return $ [(bnd, True)]
+  BooM.BoolMapTerms ts -> liftM NE.toList $ forM ts $ \(e, p) -> do
+    eE <- f e
+    return $ (eE, p == BooM.Positive)

From 6e54d1488b5a77773575794103227571c39c4609 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 17:42:12 -0700
Subject: [PATCH 11/20] avoid redundant let-bindings

---
 macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs | 58 ++++++++++++--------
 1 file changed, 36 insertions(+), 22 deletions(-)

diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
index 3ebf7a39..cdc7686d 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH/Monad.hs
@@ -239,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")
-  let res = VarE n
-  St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> BindS (VarP n) e
-                       , expressionCache = M.insert (Some elt) res (expressionCache s)
-                       }
-  return (EagerBoundExp res)
+  case e of
+    AppE f (VarE n) | pureFn == f -> return $ EagerBoundExp $ VarE n
+    _ -> do
+      n <- liftQ (newName "val")
+      let res = VarE n
+      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")
-  let res = VarE n
-  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)
+  case e of
+    VarE n -> return $ EagerBoundExp $ VarE n
+    _ -> do
+      n <- liftQ (newName "lval")
+      let res = VarE n
+      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")
-  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)
+  pureFn <- liftQ $ [| pure |]
+  case e of
+    AppE f (VarE n) | pureFn == f -> return $ EagerBoundExp $ VarE n
+    _ -> do
+      n <- liftQ (newName "lval")
+      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")
-  St.modify' $ \s -> s { accumulatedStatements = accumulatedStatements s Seq.|> LetS [ValD (VarP n) (NormalB e) []]
-                       }
-  return (LazyBoundExp (VarE n))
+  case e of
+    VarE n -> return $ LazyBoundExp $ VarE n
+    _ -> do
+     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

From f53ea84cd90ae60151e541c9c496c7c6b4055c4b Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 18:01:32 -0700
Subject: [PATCH 12/20] module import cleanup

---
 .../src/Data/Macaw/ARM/Semantics/ARMSemantics.hs      |  3 +--
 macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs      |  8 +++-----
 macaw-semmc/src/Data/Macaw/SemMC/TH.hs                | 11 ++++-------
 3 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs
index 7c47f918..a70215f5 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/ARMSemantics.hs
+++ b/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 )
@@ -63,7 +63,6 @@ execInstruction =
                                   , archTypeQ = [t| ARMSem.AArch32 |]
                                   , genLibraryFunction = notVecLib
                                   , genOpcodeCase = notVecOpc
-                                  , getExprFields = Just $ getFlds
                                   , archTranslateType = armTranslateType
                                   }
 
diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
index 5593cc61..b667c8ee 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
+++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
@@ -19,9 +19,7 @@ module Data.Macaw.ARM.Semantics.TH
     , getSIMD
     , setSIMD
     , loadSemantics
-    , armGetFields
     , armTranslateType
-    , FieldGetter(..)
     )
     where
 
@@ -37,7 +35,6 @@ import           Data.Macaw.SemMC.TH ( addEltTH, natReprTH, symFnName, translate
 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
@@ -410,6 +407,7 @@ armNonceAppEval bvi nonceApp =
           _ -> Nothing
       _ -> Nothing -- fallback to default handling
 
+
 natReprFromIntTH :: Int -> Q Exp
 natReprFromIntTH i = [| knownNat :: M.NatRepr $(litT (numTyLit (fromIntegral i))) |]
 
@@ -619,11 +617,11 @@ armAppEvaluator endianness interps elt =
           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.:> _)) <- WT.exprType struct -> Just $ do
+          (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 $ WT.exprType struct
+        WT.BaseStructRepr reprs <- return $ WB.exprType struct
         bnd <- lookupElt struct >>= \case
           Just bnd -> return bnd
           Nothing -> do
diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
index f040beee..0a05d0a0 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
@@ -38,10 +38,7 @@ module Data.Macaw.SemMC.TH (
   symFnName,
   asName,
   translateBaseType,
-  translateBaseTypeRepr,
-  sequenceAFC,
-  AppFC(..),
-  execAppFC
+  translateBaseTypeRepr
   ) where
 
 import           GHC.TypeLits ( Symbol )
@@ -922,7 +919,7 @@ defaultAppEvaluator endianness elt interps = case elt of
               return $ [(y, BVS.asUnsigned mul)]
             one = case fl of
               SR.BVArithRepr -> 1
-              SR.BVBitsRepr -> WT.maxUnsigned w 
+              SR.BVBitsRepr -> SI.maxUnsigned w 
             sval v = do
               bnd <- EagerBoundExp <$> liftQ [| M.BVValue $(natReprTH w) $(lift (BVS.asUnsigned v)) |]
               return $ [(bnd, one)]
@@ -989,14 +986,14 @@ defaultAppEvaluator endianness elt interps = case elt of
 data BoolMapOp = AndOp | OrOp
 
 
-evalBoolMap :: A.Architecture arch
+_evalBoolMap :: A.Architecture arch
             => M.Endianness
             -> BoundVarInterpretations arch t fs
             -> BoolMapOp
             -> Bool
             -> BooM.BoolMap (S.Expr t)
             -> MacawQ arch t fs BoundExp
-evalBoolMap endianness interps op defVal bmap =
+_evalBoolMap endianness interps op defVal bmap =
   case BooM.viewBoolMap bmap of
     BooM.BoolMapUnit ->     letTH [| G.addExpr (boolBase $(lift defVal)) |]
     BooM.BoolMapDualUnit -> letTH [| G.addExpr (bNotBase $(lift defVal)) |]

From 278d365a316247dbd39b438bfc5e20d79dd4cd54 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Mon, 27 Jul 2020 18:12:27 -0700
Subject: [PATCH 13/20] aarch32: simplify write action representation

---
 .../src/Data/Macaw/ARM/Semantics/TH.hs        | 38 ++++++-------------
 1 file changed, 12 insertions(+), 26 deletions(-)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
index b667c8ee..cbecfe87 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
+++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
@@ -370,7 +370,6 @@ armNonceAppEval bvi nonceApp =
             | Ctx.Empty Ctx.:> simds <- args -> Just $ do
                 simds' <- addEltTH M.LittleEndian bvi simds
                 appendStmt $ [| join (execWriteAction <$> $(refBinding simds')) |]
-                appendStmt [| setWriteMode WriteNone |]
                 liftQ [| return $ M.BoolValue True |]
 
           "uf_update_memory"
@@ -412,15 +411,9 @@ natReprFromIntTH :: Int -> Q Exp
 natReprFromIntTH i = [| knownNat :: M.NatRepr $(litT (numTyLit (fromIntegral i))) |]
 
 
-data ARMWriteActionK =
-    ARMWriteGPRsK
-  | ARMWriteMemoryK
-  | ARMWriteSIMDsK
-
-data ARMWriteActionRepr (tp :: ARMWriteActionK) where
-  ARMWriteGPRs :: ARMWriteActionRepr 'ARMWriteGPRsK
-  ARMWriteMemory :: ARMWriteActionRepr 'ARMWriteMemoryK
-  ARMWriteSIMDs :: ARMWriteActionRepr 'ARMWriteSIMDsK
+data ARMWriteGPRs = ARMWriteGPRs
+data ARMWriteMemory = ARMWriteMemory
+data ARMWriteSIMDs = ARMWriteSIMDs
 
 newtype ARMWriteAction ids s tp where
   ARMWriteAction :: G.Generator ARM.AArch32 ids s tp -> ARMWriteAction ids s tp
@@ -429,28 +422,21 @@ newtype ARMWriteAction ids s tp where
 execWriteAction :: ARMWriteAction ids s tp -> G.Generator ARM.AArch32 ids s tp
 execWriteAction (ARMWriteAction f) = f
 
-data WriteMode =
-  WriteNone
-  | WriteGPRs
-  | WriteSIMDs
-  | WriteMemory
-  deriving (Show, Eq, Lift)
-
 writeMem :: 1 <= w
          => M.NatRepr w
-         -> ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteMemoryK)
+         -> ARMWriteAction ids s ARMWriteMemory
          -> M.Value ARM.AArch32 ids (M.BVType 32)
          -> M.Value ARM.AArch32 ids (M.BVType (8 TL.* w))
-         -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteMemoryK))
+         -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s ARMWriteMemory)
 writeMem sz mem addr val = return $ do
   _ <- mem
   ARMWriteAction $ G.addStmt (M.WriteMem addr (M.BVMemRepr sz M.LittleEndian) val)
   return $ ARMWriteMemory
 
-setGPR :: ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteGPRsK)
+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 (ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteGPRsK))
+       -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s ARMWriteGPRs)
 setGPR handle regid v = do
   reg <- case regid of
     M.BVValue w i
@@ -472,10 +458,10 @@ getGPR v = do
     _ ->  E.throwError (G.GeneratorMessage $ "Bad GPR identifier (uf_gpr_get): " <> show (M.ppValueAssignments v))
   G.getRegSnapshotVal reg
 
-setSIMD :: ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteSIMDsK)
+setSIMD :: ARMWriteAction ids s ARMWriteSIMDs
         -> M.Value ARM.AArch32 ids (M.BVType 8)
         -> M.Value ARM.AArch32 ids (M.BVType 128)
-        -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s (ARMWriteActionRepr 'ARMWriteSIMDsK))
+        -> G.Generator ARM.AArch32 ids s (ARMWriteAction ids s ARMWriteSIMDs)
 setSIMD handle regid v = do
   reg <- case regid of
     M.BVValue w i
@@ -566,11 +552,11 @@ armTranslateType idsTy sTy tp = case tp of
     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) (ARMWriteActionRepr 'ARMWriteMemoryK) |]
+          [t| ARMWriteAction $(idsTy) $(sTy) ARMWriteMemory |]
       _ | Just Refl <- testEquality tp' (knownRepr :: WT.BaseTypeRepr ASL.AllSIMDBaseType) ->
-          [t| ARMWriteAction $(idsTy) $(sTy) (ARMWriteActionRepr 'ARMWriteSIMDsK) |]
+          [t| ARMWriteAction $(idsTy) $(sTy) ARMWriteSIMDs |]
       _ | Just Refl <- testEquality tp' (knownRepr :: WT.BaseTypeRepr ASL.AllGPRBaseType) ->
-          [t| ARMWriteAction $(idsTy) $(sTy) (ARMWriteActionRepr 'ARMWriteGPRsK) |]
+          [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

From dd8b78bb7bf391dd6f82e492f26be48e204be8ad Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Tue, 28 Jul 2020 10:24:59 -0700
Subject: [PATCH 14/20] aarch32: fix floating point uf calls

---
 macaw-aarch32/src/Data/Macaw/ARM/Arch.hs      |  4 +-
 .../src/Data/Macaw/ARM/Semantics/TH.hs        | 57 ++++++++++---------
 2 files changed, 31 insertions(+), 30 deletions(-)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs b/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
index a3690674..ac455b68 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
+++ b/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
diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
index cbecfe87..2734c967 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
+++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
@@ -148,7 +148,7 @@ armNonceAppEval bvi nonceApp =
               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
@@ -159,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"
 
 
@@ -169,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
@@ -177,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
@@ -185,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
@@ -193,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 ->
@@ -202,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
@@ -210,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
@@ -218,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
@@ -226,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 ->
@@ -234,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
-                  liftQ [| G.addExpr =<< (FPRecipStep knownNat <$> $(refBinding op1e) <*> $(refBinding fpcre)) |]
+                  op2e <- addEltTH M.LittleEndian bvi op2
+                  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 ->
@@ -271,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
@@ -279,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
@@ -287,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
@@ -295,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
@@ -303,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" ->
@@ -312,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
@@ -322,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
@@ -332,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
@@ -340,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
@@ -349,9 +350,9 @@ 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"
-                
+
 
           "uf_init_gprs" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteGPRs) |]
           "uf_init_memory" -> Just $ liftQ [| return $ ARMWriteAction (return ARMWriteMemory)|]

From 44c2536f3079124c60be496cefd32db642a20002 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Tue, 28 Jul 2020 10:23:04 -0700
Subject: [PATCH 15/20] add default arch type override for ppc

---
 macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs | 1 +
 macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs | 1 +
 2 files changed, 2 insertions(+)

diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs
index c2bcaedf..bd823fb3 100644
--- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs
+++ b/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
diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs
index 5e9fd948..44acf3da 100644
--- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs
+++ b/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

From 626071e459a08cc5364c511155a7d9fdf2ead566 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Tue, 28 Jul 2020 12:40:52 -0700
Subject: [PATCH 16/20] bump submodules

---
 deps/asl-translator | 2 +-
 deps/semmc          | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/deps/asl-translator b/deps/asl-translator
index 808f2d2e..94e83355 160000
--- a/deps/asl-translator
+++ b/deps/asl-translator
@@ -1 +1 @@
-Subproject commit 808f2d2ea51ec0c8fd60a32a5d9b944274e166b9
+Subproject commit 94e83355528be0992f7bcbf825809602c44b3e91
diff --git a/deps/semmc b/deps/semmc
index 6506a5d2..eb09935b 160000
--- a/deps/semmc
+++ b/deps/semmc
@@ -1 +1 @@
-Subproject commit 6506a5d2c68fdbc8d3a9f64c841e08754d1aecc0
+Subproject commit eb09935b0711c00284e42583656e5135fdd8d0a2

From f2defdcdc494392e0a404e207bbc4f0a8737a59a Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Wed, 29 Jul 2020 14:01:44 -0700
Subject: [PATCH 17/20] aarch32: use empty tuple for unit type

---
 macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs       | 10 +++++++---
 macaw-aarch32/src/Data/Macaw/ARM/Eval.hs         |  1 -
 macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs | 11 +++++++----
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs b/macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs
index 0eed22c9..edc515a2 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs
+++ b/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
diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Eval.hs b/macaw-aarch32/src/Data/Macaw/ARM/Eval.hs
index 4f59141d..d8c26564 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Eval.hs
+++ b/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 &
diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
index 2734c967..940c61f4 100644
--- a/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
+++ b/macaw-aarch32/src/Data/Macaw/ARM/Semantics/TH.hs
@@ -365,19 +365,19 @@ armNonceAppEval bvi nonceApp =
             | Ctx.Empty Ctx.:> gprs <- args -> Just $ do
                 gprs' <- addEltTH M.LittleEndian bvi gprs
                 appendStmt $ [| join (execWriteAction <$> $(refBinding gprs')) |]
-                liftQ [| return $ M.BoolValue True |]
+                liftQ [| return $ unitValue |]
                   
           "uf_update_simds"
             | Ctx.Empty Ctx.:> simds <- args -> Just $ do
                 simds' <- addEltTH M.LittleEndian bvi simds
                 appendStmt $ [| join (execWriteAction <$> $(refBinding simds')) |]
-                liftQ [| return $ M.BoolValue True |]
+                liftQ [| return $ unitValue |]
 
           "uf_update_memory"
             | Ctx.Empty Ctx.:> mem <- args -> Just $ do
                 mem' <- addEltTH M.LittleEndian bvi mem
                 appendStmt $ [| join (execWriteAction <$> $(refBinding mem')) |]
-                liftQ [| return $ M.BoolValue True |]
+                liftQ [| return $ unitValue |]
 
           "uf_noop" | Ctx.Empty <- args -> Just $ liftQ [| return $ M.BoolValue True |]
 
@@ -385,7 +385,7 @@ armNonceAppEval bvi nonceApp =
             | Ctx.Empty Ctx.:> u1 Ctx.:> u2 <- args -> Just $ do
                 _ <- addEltTH M.LittleEndian bvi u1
                 _ <- addEltTH M.LittleEndian bvi u2
-                liftQ [| return $ M.BoolValue True |]
+                liftQ [| return $ unitValue |]
           _ | "uf_assertBV_" `isPrefixOf` fnName ->
             case args of
               Ctx.Empty Ctx.:> assert Ctx.:> bv -> Just $ do
@@ -408,6 +408,9 @@ armNonceAppEval bvi nonceApp =
       _ -> 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))) |]
 

From f1d3bb61da087cb02836a276c3a6d5e081dc7cd9 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Wed, 29 Jul 2020 14:40:36 -0700
Subject: [PATCH 18/20] delete dead code

---
 macaw-semmc/src/Data/Macaw/SemMC/TH.hs | 46 --------------------------
 1 file changed, 46 deletions(-)

diff --git a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
index 0a05d0a0..e1b5920d 100644
--- a/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+++ b/macaw-semmc/src/Data/Macaw/SemMC/TH.hs
@@ -983,52 +983,6 @@ defaultAppEvaluator endianness elt interps = case elt of
 
 ----------------------------------------------------------------------
 
-data BoolMapOp = AndOp | OrOp
-
-
-_evalBoolMap :: A.Architecture arch
-            => M.Endianness
-            -> BoundVarInterpretations arch t fs
-            -> BoolMapOp
-            -> Bool
-            -> BooM.BoolMap (S.Expr t)
-            -> MacawQ arch t fs BoundExp
-_evalBoolMap endianness interps op defVal bmap =
-  case BooM.viewBoolMap bmap of
-    BooM.BoolMapUnit ->     letTH [| G.addExpr (boolBase $(lift defVal)) |]
-    BooM.BoolMapDualUnit -> letTH [| G.addExpr (bNotBase $(lift defVal)) |]
-    BooM.BoolMapTerms ts ->
-         do d <- letTH [| G.addExpr (boolBase $(lift defVal)) |]
-            F.foldl (joinBool endianness interps op) (return d) ts
-
-
-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)) |]
-
-
-
-
-
 getBVOps ::  1 SI.<= n
          => CT.NatRepr n
          -> SR.BVFlavorRepr t

From 53db924e77198de04bfd5b0852b7a6cef1774cf4 Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Thu, 30 Jul 2020 16:02:23 -0700
Subject: [PATCH 19/20] add macaw-asl-tests to travis CI

---
 .travis.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.travis.yml b/.travis.yml
index 9eac8018..b9982388 100644
--- a/.travis.yml
+++ b/.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

From 68193b9ef9c371d3ac0c846e78df2611bc0e016e Mon Sep 17 00:00:00 2001
From: Daniel Matichuk <dmatichuk@galois.com>
Date: Fri, 31 Jul 2020 00:32:26 -0700
Subject: [PATCH 20/20] bump submodules

---
 deps/asl-translator | 2 +-
 deps/dismantle      | 2 +-
 deps/semmc          | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/deps/asl-translator b/deps/asl-translator
index 94e83355..d0bac677 160000
--- a/deps/asl-translator
+++ b/deps/asl-translator
@@ -1 +1 @@
-Subproject commit 94e83355528be0992f7bcbf825809602c44b3e91
+Subproject commit d0bac677e038a54f47af0467e68c4aab95a32d64
diff --git a/deps/dismantle b/deps/dismantle
index 21c5d44d..1f61d725 160000
--- a/deps/dismantle
+++ b/deps/dismantle
@@ -1 +1 @@
-Subproject commit 21c5d44d2fdfe5bfbed6278668ddd433668218a9
+Subproject commit 1f61d7259228bbfb51053e7c990fac6d9228e154
diff --git a/deps/semmc b/deps/semmc
index eb09935b..990ce7ab 160000
--- a/deps/semmc
+++ b/deps/semmc
@@ -1 +1 @@
-Subproject commit eb09935b0711c00284e42583656e5135fdd8d0a2
+Subproject commit 990ce7ab63dd67cf0f23876d5d4d93da507ec11e