GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-18 03:21:49 +03:00
Code Issues Projects Releases Wiki Activity

Convert from applicative to nested binds in the TH code

Browse Source 
This makes the generated splices much easier to read, which will be helpful for debugging.
This commit is contained in:
Tristan Ravitch 2017-10-18 22:40:53 -07:00
parent 28b7b68881
commit ffaa912b74
1 changed files with 167 additions and 89 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

256
macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
View File

@ -272,7 +272,7 @@ addExpr expr = do
return $ M.AssignedValue assignment return $ M.AssignedValue assignment
natReprTH :: M.NatRepr w -> Q Exp natReprTH :: M.NatRepr w -> Q Exp
natReprTH w = [| knownNat :: M.NatRepr $(litT (return $ NumTyLit (natValue w))) |] natReprTH w = [| knownNat :: M.NatRepr $(litT (numTyLit (natValue w))) |]
natReprFromIntTH :: Int -> Q Exp natReprFromIntTH :: Int -> Q Exp
natReprFromIntTH i = [| knownNat :: M.NatRepr $(litT (numTyLit (fromIntegral i))) |] natReprFromIntTH i = [| knownNat :: M.NatRepr $(litT (numTyLit (fromIntegral i))) |]
@ -300,26 +300,24 @@ translateFormula ipVarName semantics interps varNames = do
translateDefinition (Map.Pair param expr) = do translateDefinition (Map.Pair param expr) = do
case param of case param of
OperandParameter _w idx -> do OperandParameter _w idx -> do
e <- addEltTH interps expr
let FreeParamF name = varNames `SL.indexShapedList` idx let FreeParamF name = varNames `SL.indexShapedList` idx
[| do val <- $(return e) [| do val <- $(addEltTH interps expr)
let reg = toPPCReg $(varE name) let reg = toPPCReg $(varE name)
curPPCState . M.boundValue reg .= val |] curPPCState . M.boundValue reg .= val
|]
LiteralParameter APPC.LocMem -> writeMemTH interps expr LiteralParameter APPC.LocMem -> writeMemTH interps expr
LiteralParameter loc -> do LiteralParameter loc -> do
e <- addEltTH interps expr [| do val <- $(addEltTH interps expr)
reg <- locToRegTH (Proxy @arch) loc curPPCState . M.boundValue $(locToRegTH (Proxy @arch) loc) .= val
[| do val <- $(return e) |]
curPPCState . M.boundValue $(return reg) .= val |]
FunctionParameter str (WrappedOperand _ opIx) _w -> do FunctionParameter str (WrappedOperand _ opIx) _w -> do
let FreeParamF boundOperandName = SL.indexShapedList varNames opIx let FreeParamF boundOperandName = SL.indexShapedList varNames opIx
case lookup str (A.locationFuncInterpretation (Proxy @arch)) of case lookup str (A.locationFuncInterpretation (Proxy @arch)) of
Nothing -> [| error ("Function has no definition: " ++ show $(lift str)) |] Nothing -> [| error ("Function has no definition: " ++ show $(lift str)) |]
Just fi -> do Just fi -> do
e <- addEltTH interps expr
[| do case $(varE (A.exprInterpName fi)) $(varE boundOperandName) of [| do case $(varE (A.exprInterpName fi)) $(varE boundOperandName) of
Just reg -> do Just reg -> do
val <- $(return e) val <- $(addEltTH interps expr)
curPPCState . M.boundValue (toPPCReg reg) .= val curPPCState . M.boundValue (toPPCReg reg) .= val
Nothing -> error ("Invalid instruction form at " ++ show $(varE ipVarName)) Nothing -> error ("Invalid instruction form at " ++ show $(varE ipVarName))
|] |]
@ -349,6 +347,9 @@ addEltTH interps elt = case elt of
S.NonceAppElt n -> evalNonceAppTH interps (S.nonceEltApp n) S.NonceAppElt n -> evalNonceAppTH interps (S.nonceEltApp n)
S.SemiRingLiteral {} -> [| error "SemiRingLiteral Elts are not supported" |] S.SemiRingLiteral {} -> [| error "SemiRingLiteral Elts are not supported" |]
symFnName :: S.SimpleSymFn t args ret -> String
symFnName = T.unpack . Sy.solverSymbolAsText . S.symFnName
writeMemTH :: forall arch t tp writeMemTH :: forall arch t tp
. (L.Location arch ~ APPC.Location arch, . (L.Location arch ~ APPC.Location arch,
A.Architecture arch, A.Architecture arch,
@ -362,7 +363,7 @@ writeMemTH bvi expr =
S.NonceAppElt n -> S.NonceAppElt n ->
case S.nonceEltApp n of case S.nonceEltApp n of
S.FnApp symFn args S.FnApp symFn args
| Just memWidth <- matchWriteMemWidth (T.unpack (Sy.solverSymbolAsText (S.symFnName symFn))) -> | Just memWidth <- matchWriteMemWidth (symFnName symFn) ->
case FC.toListFC Some args of case FC.toListFC Some args of
[_, Some addr, Some val] -> [_, Some addr, Some val] ->
[| do addrVal <- $(addEltTH bvi addr) [| do addrVal <- $(addEltTH bvi addr)
@ -391,7 +392,7 @@ evalNonceAppTH :: forall arch t tp
evalNonceAppTH bvi nonceApp = evalNonceAppTH bvi nonceApp =
case nonceApp of case nonceApp of
S.FnApp symFn args -> do S.FnApp symFn args -> do
let fnName = T.unpack (Sy.solverSymbolAsText (S.symFnName symFn)) let fnName = symFnName symFn
-- Recursively evaluate the arguments. In the recursive evaluator, we -- Recursively evaluate the arguments. In the recursive evaluator, we
-- expect two cases: -- expect two cases:
-- --
@ -420,14 +421,13 @@ evalNonceAppTH bvi nonceApp =
S.NonceAppElt nonceApp' -> do S.NonceAppElt nonceApp' -> do
case S.nonceEltApp nonceApp' of case S.nonceEltApp nonceApp' of
S.FnApp symFn' args' -> do S.FnApp symFn' args' -> do
let recName = T.unpack (Sy.solverSymbolAsText (S.symFnName symFn')) let recName = symFnName symFn'
case lookup recName (A.locationFuncInterpretation (Proxy @arch)) of case lookup recName (A.locationFuncInterpretation (Proxy @arch)) of
Nothing -> fail ("Unsupported UF: " ++ recName) Nothing -> fail ("Unsupported UF: " ++ recName)
Just fi -> do Just fi -> do
let argNames = FC.toListFC (asName fnName bvi) args' case FC.toListFC (asName fnName bvi) args' of
case argNames of
[] -> fail ("zero-argument uninterpreted functions are not supported: " ++ fnName) [] -> fail ("zero-argument uninterpreted functions are not supported: " ++ fnName)
_ -> do argNames -> do
let call = appE (varE (A.exprInterpName fi)) $ foldr1 appE (map varE argNames) let call = appE (varE (A.exprInterpName fi)) $ foldr1 appE (map varE argNames)
[| extractValue (PE.interpIsR0 ($(call))) |] [| extractValue (PE.interpIsR0 ($(call))) |]
_ -> fail ("Unsupported nonce app type") _ -> fail ("Unsupported nonce app type")
@ -453,10 +453,9 @@ evalNonceAppTH bvi nonceApp =
-- args is an assignment that contains elts; we could just generate -- args is an assignment that contains elts; we could just generate
-- expressions that evaluate each one and then splat them into new names -- expressions that evaluate each one and then splat them into new names
-- that we apply our name to. -- that we apply our name to.
let argNames = FC.toListFC (asName fnName bvi) args case FC.toListFC (asName fnName bvi) args of
case argNames of
[] -> fail ("zero-argument uninterpreted functions are not supported: " ++ fnName) [] -> fail ("zero-argument uninterpreted functions are not supported: " ++ fnName)
_ -> do argNames -> do
let call = appE (varE (A.exprInterpName fi)) $ foldr1 appE (map varE argNames) let call = appE (varE (A.exprInterpName fi)) $ foldr1 appE (map varE argNames)
[| extractValue ($(call)) |] [| extractValue ($(call)) |]
_ -> [| error "Unsupported NonceApp case" |] _ -> [| error "Unsupported NonceApp case" |]
@ -479,56 +478,86 @@ floatingPointTH bvi fnName args =
[Some a] -> [Some a] ->
case fnName of case fnName of
"round_single" -> "round_single" ->
[| addExpr =<< AppExpr <$> (M.FPCvt M.DoubleFloatRepr <$> $(addEltTH bvi a) <*> pure M.SingleFloatRepr) |] [| do fpval <- $(addEltTH bvi a)
addExpr (AppExpr (M.FPCvt M.DoubleFloatRepr fpval M.SingleFloatRepr))
|]
"abs" -> "abs" ->
-- Note that fabs is only defined for doubles; the operation is the -- Note that fabs is only defined for doubles; the operation is the
-- same for single and double precision on PPC, so there is only a -- same for single and double precision on PPC, so there is only a
-- single instruction. -- single instruction.
[| do e <- AppExpr <$> (M.FPAbs M.DoubleFloatRepr <$> $(addEltTH bvi a)) [| do fpval <- $(addEltTH bvi a)
addExpr e addExpr (AppExpr (M.FPAbs M.DoubleFloatRepr fpval))
|] |]
"negate64" -> "negate64" ->
[| do val <- $(addEltTH bvi a) [| do fpval <- $(addEltTH bvi a)
addExpr (AppExpr (M.FPNeg M.DoubleFloatRepr val)) addExpr (AppExpr (M.FPNeg M.DoubleFloatRepr fpval))
|] |]
"negate32" -> "negate32" ->
[| addExpr =<< (AppExpr <$> (M.FPNeg M.SingleFloatRepr <$> $(addEltTH bvi a))) |] [| do fpval <- $(addEltTH bvi a)
addExpr (AppExpr (M.FPNeg M.SingleFloatRepr fpval))
|]
_ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName) _ -> fail ("Unsupported unary floating point intrinsic: " ++ fnName)
[Some a, Some b] -> [Some a, Some b] ->
case fnName of case fnName of
"add64" -> "add64" ->
[| addExpr =<< AppExpr <$> (M.FPAdd M.DoubleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPAdd M.DoubleFloatRepr valA valB))
|]
"add32" -> "add32" ->
[| addExpr =<< AppExpr <$> (M.FPAdd M.SingleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPAdd M.SingleFloatRepr valA valB))
|]
"sub64" -> "sub64" ->
[| addExpr =<< AppExpr <$> (M.FPSub M.DoubleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPSub M.DoubleFloatRepr valA valB))
|]
"sub32" -> "sub32" ->
[| addExpr =<< AppExpr <$> (M.FPSub M.SingleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPSub M.SingleFloatRepr valA valB))
|]
"mul64" -> "mul64" ->
[| addExpr =<< AppExpr <$> (M.FPMul M.DoubleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPMul M.DoubleFloatRepr valA valB))
|]
"mul32" -> "mul32" ->
[| addExpr =<< AppExpr <$> (M.FPMul M.SingleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPMul M.SingleFloatRepr valA valB))
|]
"div64" -> "div64" ->
[| addExpr =<< AppExpr <$> (M.FPDiv M.DoubleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPDiv M.DoubleFloatRepr valA valB))
|]
"div32" -> "div32" ->
[| addExpr =<< AppExpr <$> (M.FPDiv M.SingleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi b)) |] [| do valA <- $(addEltTH bvi a)
valB <- $(addEltTH bvi b)
addExpr (AppExpr (M.FPDiv M.SingleFloatRepr valA valB))
|]
_ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName) _ -> fail ("Unsupported binary floating point intrinsic: " ++ fnName)
[Some a, Some b, Some c] -> [Some a, Some b, Some c] ->
case fnName of case fnName of
"muladd64" -> "muladd64" ->
-- FIXME: This is very wrong - we need a separate constructor for it -- FIXME: This is very wrong - we need a separate constructor for it
-- a * c + b -- a * c + b
[| do prod <- AppExpr <$> (M.FPMul M.DoubleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi c)) [| do valA <- $(addEltTH bvi a)
prodVal <- addExpr prod valB <- $(addEltTH bvi b)
e <- AppExpr <$> (M.FPAdd M.DoubleFloatRepr prodVal <$> $(addEltTH bvi b)) valC <- $(addEltTH bvi c)
addExpr e prodVal <- addExpr (AppExpr (M.FPMul M.DoubleFloatRepr valA valC))
addExpr (AppExpr (M.FPAdd M.DoubleFloatRepr prodVal valB))
|] |]
"muladd32" -> "muladd32" ->
-- a * c + b -- a * c + b
[| do prod <- AppExpr <$> (M.FPMul M.SingleFloatRepr <$> $(addEltTH bvi a) <*> $(addEltTH bvi c)) [| do valA <- $(addEltTH bvi a)
prodVal <- addExpr prod valB <- $(addEltTH bvi b)
e <- AppExpr <$> (M.FPAdd M.SingleFloatRepr prodVal <$> $(addEltTH bvi b)) valC <- $(addEltTH bvi c)
addExpr e prodVal <- addExpr (AppExpr (M.FPMul M.SingleFloatRepr valA valC))
addExpr (AppExpr (M.FPAdd M.SingleFloatRepr prodVal valB))
|] |]
_ -> fail ("Unsupported ternary floating point intrinsic: " ++ fnName) _ -> fail ("Unsupported ternary floating point intrinsic: " ++ fnName)
_ -> fail ("Unsupported floating point intrinsic: " ++ fnName) _ -> fail ("Unsupported floating point intrinsic: " ++ fnName)
@ -577,27 +606,47 @@ crucAppToExprTH elt interps = case elt of
S.TrueBool -> [| return $ ValueExpr (M.BoolValue True) |] S.TrueBool -> [| return $ ValueExpr (M.BoolValue True) |]
S.FalseBool -> [| return $ ValueExpr (M.BoolValue False) |] S.FalseBool -> [| return $ ValueExpr (M.BoolValue False) |]
S.NotBool bool -> S.NotBool bool ->
[| AppExpr <$> (M.NotApp <$> $(addEltTH interps bool)) |] [| do bval <- $(addEltTH interps bool)
return (AppExpr (M.NotApp bval))
|]
S.AndBool bool1 bool2 -> S.AndBool bool1 bool2 ->
[| AppExpr <$> (M.AndApp <$> $(addEltTH interps bool1) <*> $(addEltTH interps bool2)) |] [| do bval1 <- $(addEltTH interps bool1)
bval2 <- $(addEltTH interps bool2)
return (AppExpr (M.AndApp bval1 bval2))
|]
S.XorBool bool1 bool2 -> S.XorBool bool1 bool2 ->
[| AppExpr <$> (M.XorApp <$> $(addEltTH interps bool1) <*> $(addEltTH interps bool2)) |] [| do bval1 <- $(addEltTH interps bool1)
bval2 <- $(addEltTH interps bool2)
return (AppExpr (M.XorApp bval1 bval2))
|]
S.IteBool test t f -> S.IteBool test t f ->
[| AppExpr <$> (M.Mux M.BoolTypeRepr [| do testVal <- $(addEltTH interps test)
<$> $(addEltTH interps test) tval <- $(addEltTH interps t)
<*> $(addEltTH interps t) fval <- $(addEltTH interps f)
<*> $(addEltTH interps f)) |] return (AppExpr (M.Mux M.BoolTypeRepr testVal tval fval))
|]
S.BVIte w numBranches test t f -> S.BVIte w numBranches test t f ->
[| AppExpr <$> (M.Mux (M.BVTypeRepr $(natReprTH w)) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps test) testVal <- $(addEltTH interps test)
<*> $(addEltTH interps t) tval <- $(addEltTH interps t)
<*> $(addEltTH interps f)) |] fval <- $(addEltTH interps f)
return (AppExpr (M.Mux (M.BVTypeRepr rep) testVal tval fval))
|]
S.BVEq bv1 bv2 -> S.BVEq bv1 bv2 ->
[| AppExpr <$> (M.Eq <$> $(addEltTH interps bv1) <*> $(addEltTH interps bv2)) |] [| do bval1 <- $(addEltTH interps bv1)
bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.Eq bval1 bval2))
|]
S.BVSlt bv1 bv2 -> S.BVSlt bv1 bv2 ->
[| AppExpr <$> (M.BVSignedLt <$> $(addEltTH interps bv1) <*> $(addEltTH interps bv2)) |] [| do bval1 <- $(addEltTH interps bv1)
bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVSignedLt bval1 bval2))
|]
S.BVUlt bv1 bv2 -> S.BVUlt bv1 bv2 ->
[| AppExpr <$> (M.BVUnsignedLt <$> $(addEltTH interps bv1) <*> $(addEltTH interps bv2)) |] [| do bval1 <- $(addEltTH interps bv1)
bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVUnsignedLt bval1 bval2))
|]
S.BVConcat w bv1 bv2 -> do S.BVConcat w bv1 bv2 -> do
let u = S.bvWidth bv1 let u = S.bvWidth bv1
v = S.bvWidth bv2 v = S.bvWidth bv2
@ -618,8 +667,7 @@ crucAppToExprTH elt interps = case elt of
let w = S.bvWidth bv let w = S.bvWidth bv
case natValue n + 1 <= natValue w of case natValue n + 1 <= natValue w of
True -> True ->
[| do let foo = "BVSelect" [| do bvVal <- $(addEltTH interps bv)
bvVal <- $(addEltTH interps bv)
Just S.LeqProof <- return $ S.testLeq ($(natReprTH n) `addNat` (knownNat @1)) $(natReprTH w) Just S.LeqProof <- return $ S.testLeq ($(natReprTH n) `addNat` (knownNat @1)) $(natReprTH w)
pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl $(natReprTH idx)) (S.leqProof (knownNat @1) $(natReprTH n)) pf1@S.LeqProof <- return $ S.leqAdd2 (S.leqRefl $(natReprTH idx)) (S.leqProof (knownNat @1) $(natReprTH n))
pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (knownNat @1)) $(natReprTH idx) pf2@S.LeqProof <- return $ S.leqAdd (S.leqRefl (knownNat @1)) $(natReprTH idx)
@ -637,52 +685,82 @@ crucAppToExprTH elt interps = case elt of
-- Note: This is still untested -- Note: This is still untested
[| do bvVal <- $(addEltTH interps bv) [| do bvVal <- $(addEltTH interps bv)
bvComp <- addExpr (AppExpr (M.BVComplement $(natReprTH w) bvVal)) bvComp <- addExpr (AppExpr (M.BVComplement $(natReprTH w) bvVal))
return $ AppExpr (M.BVAdd $(natReprTH w) bvComp (M.mkLit $(natReprTH w) 1)) |] return $ AppExpr (M.BVAdd $(natReprTH w) bvComp (M.mkLit $(natReprTH w) 1))
|]
S.BVTestBit idx bv -> S.BVTestBit idx bv ->
-- Note: below is untested, could be wrong. -- Note: below is untested, could be wrong.
[| do let bitExp = ValueExpr (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift idx)) [| do bitExpVal <- addExpr (ValueExpr (M.BVValue $(natReprTH (S.bvWidth bv)) $(lift idx)))
bitExpVal <- addExpr bitExp bval <- $(addEltTH interps bv)
AppExpr <$> (M.BVTestBit <$> bitExpVal <*> $(addEltTH interps bv)) |] return (AppExpr (M.BVTestBit bitExpVal bval))
|]
S.BVAdd w bv1 bv2 -> S.BVAdd w bv1 bv2 ->
[| AppExpr <$> (M.BVAdd $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVAdd rep bval1 bval2))
|]
S.BVMul w bv1 bv2 -> S.BVMul w bv1 bv2 ->
[| AppExpr <$> (M.BVMul $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVMul rep bval1 bval2))
|]
S.BVShl w bv1 bv2 -> S.BVShl w bv1 bv2 ->
[| AppExpr <$> (M.BVShl $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVShl rep bval1 bval2))
|]
S.BVLshr w bv1 bv2 -> S.BVLshr w bv1 bv2 ->
[| AppExpr <$> (M.BVShr $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVShr rep bval1 bval2))
|]
S.BVAshr w bv1 bv2 -> S.BVAshr w bv1 bv2 ->
[| AppExpr <$> (M.BVSar $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVSar rep bval1 bval2))
|]
S.BVZext w bv -> S.BVZext w bv ->
[| AppExpr <$> (M.UExt <$> $(addEltTH interps bv) <*> (pure $(natReprTH w))) |] [| do bval <- $(addEltTH interps bv)
let rep = $(natReprTH w)
return (AppExpr (M.UExt bval rep))
|]
S.BVSext w bv -> S.BVSext w bv ->
[| AppExpr <$> (M.SExt <$> $(addEltTH interps bv) <*> (pure $(natReprTH w))) |] [| do bval <- $(addEltTH interps bv)
let rep = $(natReprTH w)
return (AppExpr (M.SExt bval rep))
|]
S.BVTrunc w bv -> S.BVTrunc w bv ->
[| AppExpr <$> (M.Trunc <$> $(addEltTH interps bv) <*> (pure $(natReprTH w))) |] [| do bval <- $(addEltTH interps bv)
let rep = $(natReprTH w)
return (AppExpr (M.Trunc bval rep))
|]
S.BVBitNot w bv -> S.BVBitNot w bv ->
[| AppExpr <$> (M.BVComplement $(natReprTH w) <$> $(addEltTH interps bv)) |] [| do let rep = $(natReprTH w)
bval <- $(addEltTH interps bv)
return (AppExpr (M.BVComplement rep bval))
|]
S.BVBitAnd w bv1 bv2 -> S.BVBitAnd w bv1 bv2 ->
[| AppExpr <$> (M.BVAnd $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVAnd rep bval1 bval2))
|]
S.BVBitOr w bv1 bv2 -> S.BVBitOr w bv1 bv2 ->
[| AppExpr <$> (M.BVOr $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVOr rep bval1 bval2))
|]
S.BVBitXor w bv1 bv2 -> S.BVBitXor w bv1 bv2 ->
[| AppExpr <$> (M.BVXor $(natReprTH w) [| do let rep = $(natReprTH w)
<$> $(addEltTH interps bv1) bval1 <- $(addEltTH interps bv1)
<*> $(addEltTH interps bv2)) |] bval2 <- $(addEltTH interps bv2)
return (AppExpr (M.BVXor rep bval1 bval2))
|]
_ -> [| error "unsupported Crucible elt" |] _ -> [| error "unsupported Crucible elt" |]