Change stack and register models to bytes instead of values - #245

Open

gergo- wants to merge 15 commits into

AbsInt:masterfrom

gergo-:locmap-encoding

Commits on Aug 23, 2018

Add LTLtyping and enforce well-typed LTL in Allocation
gergo-
committed
3c5e96e
Make builtin_res type nonrecursive
gergo-
committed
bb1a7ca
Proof of type preservation on LTL.
gergo-
committed
591fafa
Adapt LTL typing proof for all architectures
gergo-
committed
02ed73f
Unify register and stack cases in Locmap.set
gergo-
committed
7c3c74e
Change Locmap to map locations to encoded bytes
gergo-
committed
3c95bcf
Simplify properties and proofs using wt_locset
gergo-
committed
fb34616
Model the register file as a block of bytes
gergo-
committed
47798ef
Change types of stack slots to quantities
gergo-
committed
fa45359
First version of "fragment block" to unify register and stack models
gergo-
committed
7e32dca
Change Locations (register file and stack) to FragmentBlock
gergo-
committed
9eb9c9f
Change Regfile to a functor, base mreg and ARM's preg on it
gergo-
committed
3b59dae
Port PowerPC's pregs to the Registerfile representation
gergo-
committed
b0d3279
Port x86's pregs to the Registerfile representation
gergo-
committed
675e82b
Port RISC-V's pregs to the Registerfile representation
gergo-
committed
8ea0903