mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-24 00:42:28 +03:00
Update to the new parameterized-utils List
This replaces the old ShapedList from dismantle-tablegen
This commit is contained in:
parent
269c329b93
commit
f1b0775be8
@ -5,6 +5,8 @@ packages: macaw-ppc/
|
|||||||
submodules/semmc/semmc-ppc/
|
submodules/semmc/semmc-ppc/
|
||||||
submodules/dismantle/dismantle-tablegen/
|
submodules/dismantle/dismantle-tablegen/
|
||||||
submodules/dismantle/dismantle-ppc/
|
submodules/dismantle/dismantle-ppc/
|
||||||
|
submodules/dismantle/dismantle-arm/
|
||||||
|
submodules/dismantle/dismantle-thumb/
|
||||||
submodules/parameterized-utils/
|
submodules/parameterized-utils/
|
||||||
submodules/crucible/crucible/
|
submodules/crucible/crucible/
|
||||||
submodules/crucible/galois-matlab/
|
submodules/crucible/galois-matlab/
|
||||||
|
@ -237,43 +237,43 @@ ppcInstructionMatcher (D.Instruction opc operands) =
|
|||||||
D.ISYNC -> Just (G.addStmt (MC.ExecArchStmt Isync))
|
D.ISYNC -> Just (G.addStmt (MC.ExecArchStmt Isync))
|
||||||
D.DCBA ->
|
D.DCBA ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
G.addStmt (MC.ExecArchStmt (Dcba ea))
|
G.addStmt (MC.ExecArchStmt (Dcba ea))
|
||||||
D.DCBF ->
|
D.DCBF ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
G.addStmt (MC.ExecArchStmt (Dcbf ea))
|
G.addStmt (MC.ExecArchStmt (Dcbf ea))
|
||||||
D.DCBI ->
|
D.DCBI ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
G.addStmt (MC.ExecArchStmt (Dcbi ea))
|
G.addStmt (MC.ExecArchStmt (Dcbi ea))
|
||||||
D.DCBST ->
|
D.DCBST ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
G.addStmt (MC.ExecArchStmt (Dcbst ea))
|
G.addStmt (MC.ExecArchStmt (Dcbst ea))
|
||||||
D.DCBZ ->
|
D.DCBZ ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
G.addStmt (MC.ExecArchStmt (Dcbz ea))
|
G.addStmt (MC.ExecArchStmt (Dcbz ea))
|
||||||
D.DCBZL ->
|
D.DCBZL ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
G.addStmt (MC.ExecArchStmt (Dcbzl ea))
|
G.addStmt (MC.ExecArchStmt (Dcbzl ea))
|
||||||
D.DCBT ->
|
D.DCBT ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.U5imm imm D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.U5imm imm D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
th <- O.extractValue imm
|
th <- O.extractValue imm
|
||||||
G.addStmt (MC.ExecArchStmt (Dcbt ea th))
|
G.addStmt (MC.ExecArchStmt (Dcbt ea th))
|
||||||
D.DCBTST ->
|
D.DCBTST ->
|
||||||
case operands of
|
case operands of
|
||||||
D.Memrr memrr D.:> D.U5imm imm D.:> D.Nil -> Just $ do
|
D.Memrr memrr D.:< D.U5imm imm D.:< D.Nil -> Just $ do
|
||||||
ea <- memrrToEffectiveAddress memrr
|
ea <- memrrToEffectiveAddress memrr
|
||||||
th <- O.extractValue imm
|
th <- O.extractValue imm
|
||||||
G.addStmt (MC.ExecArchStmt (Dcbtst ea th))
|
G.addStmt (MC.ExecArchStmt (Dcbtst ea th))
|
||||||
|
@ -42,7 +42,7 @@ import qualified Data.Parameterized.Lift as LF
|
|||||||
import qualified Data.Parameterized.Map as Map
|
import qualified Data.Parameterized.Map as Map
|
||||||
import qualified Data.Parameterized.NatRepr as NR
|
import qualified Data.Parameterized.NatRepr as NR
|
||||||
import qualified Data.Parameterized.Nonce as PN
|
import qualified Data.Parameterized.Nonce as PN
|
||||||
import qualified Data.Parameterized.ShapedList as SL
|
import qualified Data.Parameterized.List as SL
|
||||||
import Data.Parameterized.Some ( Some(..) )
|
import Data.Parameterized.Some ( Some(..) )
|
||||||
import qualified Data.Parameterized.TraversableFC as FC
|
import qualified Data.Parameterized.TraversableFC as FC
|
||||||
import Data.Parameterized.Witness ( Witness(..) )
|
import Data.Parameterized.Witness ( Witness(..) )
|
||||||
@ -184,7 +184,7 @@ genCaseBody :: forall a sh t arch
|
|||||||
-> Name
|
-> Name
|
||||||
-> a sh
|
-> a sh
|
||||||
-> ParameterizedFormula (Sym t) arch sh
|
-> ParameterizedFormula (Sym t) arch sh
|
||||||
-> SL.ShapedList (FreeParamF Name) sh
|
-> SL.List (FreeParamF Name) sh
|
||||||
-> Q Exp
|
-> Q Exp
|
||||||
genCaseBody ltr ena ae ipVarName _opc semantics varNames = do
|
genCaseBody ltr ena ae ipVarName _opc semantics varNames = do
|
||||||
regsName <- newName "_regs"
|
regsName <- newName "_regs"
|
||||||
@ -194,7 +194,7 @@ genCaseBody ltr ena ae ipVarName _opc semantics varNames = do
|
|||||||
locVarsMap = Map.foldrWithKey (collectVarForLocation (Proxy @arch)) Map.empty (pfLiteralVars semantics)
|
locVarsMap = Map.foldrWithKey (collectVarForLocation (Proxy @arch)) Map.empty (pfLiteralVars semantics)
|
||||||
|
|
||||||
opVarsMap :: Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
opVarsMap :: Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
||||||
opVarsMap = SL.foldrFCIndexed (collectOperandVars varNames) Map.empty (pfOperandVars semantics)
|
opVarsMap = SL.ifoldr (collectOperandVars varNames) Map.empty (pfOperandVars semantics)
|
||||||
|
|
||||||
collectVarForLocation :: forall tp arch proxy t
|
collectVarForLocation :: forall tp arch proxy t
|
||||||
. proxy arch
|
. proxy arch
|
||||||
@ -215,13 +215,13 @@ collectVarForLocation _ loc bv = Map.insert bv loc
|
|||||||
-- SemMC.BoundVar module for information about the nature of that change
|
-- SemMC.BoundVar module for information about the nature of that change
|
||||||
-- (basically, from 'Symbol' to BaseType).
|
-- (basically, from 'Symbol' to BaseType).
|
||||||
collectOperandVars :: forall sh tp arch t
|
collectOperandVars :: forall sh tp arch t
|
||||||
. SL.ShapedList (FreeParamF Name) sh
|
. SL.List (FreeParamF Name) sh
|
||||||
-> SL.Index sh tp
|
-> SL.Index sh tp
|
||||||
-> BV.BoundVar (Sym t) arch tp
|
-> BV.BoundVar (Sym t) arch tp
|
||||||
-> Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
-> Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
||||||
-> Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
-> Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
||||||
collectOperandVars varNames ix (BV.BoundVar bv) m =
|
collectOperandVars varNames ix (BV.BoundVar bv) m =
|
||||||
case SL.indexShapedList varNames ix of
|
case varNames SL.!! ix of
|
||||||
FreeParamF name -> Map.insert bv (FreeParamF name) m
|
FreeParamF name -> Map.insert bv (FreeParamF name) m
|
||||||
|
|
||||||
-- | Generate an implementation of 'execInstruction' that runs in the
|
-- | Generate an implementation of 'execInstruction' that runs in the
|
||||||
@ -300,7 +300,7 @@ translateFormula :: forall arch t sh .
|
|||||||
-> Name
|
-> Name
|
||||||
-> ParameterizedFormula (Sym t) arch sh
|
-> ParameterizedFormula (Sym t) arch sh
|
||||||
-> BoundVarInterpretations arch t
|
-> BoundVarInterpretations arch t
|
||||||
-> SL.ShapedList (FreeParamF Name) sh
|
-> SL.List (FreeParamF Name) sh
|
||||||
-> Q Exp
|
-> Q Exp
|
||||||
translateFormula ltr ena ae ipVarName semantics interps varNames = do
|
translateFormula ltr ena ae ipVarName semantics interps varNames = do
|
||||||
let preamble = [ bindS (varP (regsValName interps)) [| G.getRegs |] ]
|
let preamble = [ bindS (varP (regsValName interps)) [| G.getRegs |] ]
|
||||||
@ -311,7 +311,7 @@ translateFormula ltr ena ae 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
|
||||||
let FreeParamF name = varNames `SL.indexShapedList` idx
|
let FreeParamF name = varNames SL.!! idx
|
||||||
newVal <- addEltTH interps expr
|
newVal <- addEltTH interps expr
|
||||||
appendStmt [| G.setRegVal (O.toRegister $(varE name)) $(return newVal) |]
|
appendStmt [| G.setRegVal (O.toRegister $(varE name)) $(return newVal) |]
|
||||||
LiteralParameter loc
|
LiteralParameter loc
|
||||||
@ -320,7 +320,7 @@ translateFormula ltr ena ae ipVarName semantics interps varNames = do
|
|||||||
valExp <- addEltTH interps expr
|
valExp <- addEltTH interps expr
|
||||||
appendStmt [| G.setRegVal $(ltr loc) $(return valExp) |]
|
appendStmt [| G.setRegVal $(ltr loc) $(return valExp) |]
|
||||||
FunctionParameter str (WrappedOperand _ opIx) _w -> do
|
FunctionParameter str (WrappedOperand _ opIx) _w -> do
|
||||||
let FreeParamF boundOperandName = SL.indexShapedList varNames opIx
|
let FreeParamF boundOperandName = varNames SL.!! opIx
|
||||||
case lookup str (A.locationFuncInterpretation (Proxy @arch)) of
|
case lookup str (A.locationFuncInterpretation (Proxy @arch)) of
|
||||||
Nothing -> fail ("Function has no definition: " ++ str)
|
Nothing -> fail ("Function has no definition: " ++ str)
|
||||||
Just fi -> do
|
Just fi -> do
|
||||||
|
@ -1 +1 @@
|
|||||||
Subproject commit 410f4ceb253f4d908fb1e8104418e0c1fce686f0
|
Subproject commit d91a62996c5d4b5fd597f381c89488aa6e6f6319
|
@ -1 +1 @@
|
|||||||
Subproject commit e14f73980ff6a3de326d404402f1cbda63f98555
|
Subproject commit b101733e2e5ceb04f16cdf0e5b1a80983c94a976
|
@ -1 +1 @@
|
|||||||
Subproject commit 3e91cb7efffe13b08fea7e81b5aebb81a9cd625f
|
Subproject commit e1b2c3f6b1f86b38336777fafa01e0dccd444616
|
@ -1 +1 @@
|
|||||||
Subproject commit 7d6e4b93028153ec10459e7b3bf0aa7635bb3e54
|
Subproject commit 70a066a282a91b56dd96031c31bf66db788b1b88
|
Loading…
Reference in New Issue
Block a user