| A simpler RISC-style view of x86 assembly language |
Require Import List TheoryList ZArith.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.ListUtil.
Require Import Asm.Util.Monad.
Require Import Asm.Util.Maps.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.Trusted.Safety.
Require Import ProofOS.Trusted.Machine.
Require Import ProofOS.Trusted.Arches.
Require Import ProofOS.AbsInt.Bounded.
Require Import ProofOS.AbsInt.Reduce.
Set Implicit Arguments.
Types describing the SAL assembly language |
| Pseudo-registers |
Inductive salReg : Set :=
| SX86 : reg32 -> salReg
| STmp1 : salReg
| STmp2 : salReg.
| Side-effect-free expressions |
Inductive salExp : Set :=
| SConst : int32 -> salExp
| SReg : salReg -> salExp
| SArith : arith_op -> salExp -> salExp -> salExp
| SShift : shift_op -> salExp -> nat -> salExp.
| Kinds of indirect jumps, corresponding to which real x86 instruction was compiled to a SAL jump instruction |
Inductive salIJump : Set :=
| SCall
| SRet.
| Kinds of arithmetic comparisons |
Inductive salCmp : Set :=
| SWithCF
| SNoCF.
| Commands, which don't touch the program counter |
Inductive salCmd : Set :=
| SSet : salReg -> salExp -> salCmd
| SLoad : salReg -> salExp -> salCmd
| SStore : salExp -> salExp -> salCmd
| SCompare : salCmp -> arith_op -> salExp -> salExp -> salCmd.
| Jumps, which end instructions |
Inductive salJump : Set :=
| SFail : salJump
| SFallthru : salJump
| SJump : int32 -> salJump
| SIndirectJump : salIJump -> salExp -> salJump
| SConditionalJump : cc -> int32 -> salJump.
Definition salInstr := (list salCmd * salJump)%type.
Operational semantics of SAL |
Building finite maps |
Definition salReg_eq_dec : forall (r1 r2 : salReg), {r1 = r2} + {r1 <> r2}.
Module SalRegIndexed <: INDEXED_TYPE.
Definition t := salReg.
Definition index r :=
(match r with
| SX86 r' => Reg32Indexed.index r'
| STmp1 => 9
| STmp2 => 10
end)%positive.
Theorem index_inj: forall (x y: t), index x = index y -> x = y.
Definition eq := salReg_eq_dec.
Definition invert p :=
(match p with
| 9 => STmp1
| 10 => STmp2
| _ => SX86 (Reg32Indexed.invert p)
end)%positive.
Theorem invert_index : forall x, invert (index x) = x.
End SalRegIndexed.
Module SalRegMap := IMap(SalRegIndexed).
Definition salRegs := SalRegMap.t int32.
The type of SAL machine states |
Record salState : Set := {
SstRegs : salRegs;
SstFlags : flags;
SstMem : mem;
SstPc : int32
}.
Accessors and mutators |
Definition get_instr st := decode_instr (SstMem st) (SstPc st).
Definition get_reg st r :=
SalRegMap.get r (SstRegs st).
Definition set_reg st r n :=
Build_salState (SalRegMap.set r n (SstRegs st)) (SstFlags st) (SstMem st) (SstPc st).
Definition get_flag st f := FlagMap.get f (SstFlags st).
Definition set_flag st f b := Build_salState (SstRegs st)
(FlagMap.set f b (SstFlags st)) (SstMem st) (SstPc st).
Definition get_mem st a :=
Int32Map.get a (SstMem st).
Definition set_mem st a n :=
Build_salState (SstRegs st) (SstFlags st) (Int32Map.set a n (SstMem st)) (SstPc st).
Definition set_pc st pc :=
Build_salState (SstRegs st) (SstFlags st) (SstMem st) pc.
Combined 32-bit memory accessor/mutator |
Definition get_mem32 st a := get_mem32' (SstMem st) a.
Definition set_mem32 st a v :=
Build_salState (SstRegs st) (SstFlags st) (set_mem32' (SstMem st) a v) (SstPc st).
Lemma invert_set_mem32 : forall st addr v,
get_mem32 (set_mem32 st addr v) addr = v.
Theorem invert_set_mem32_neq : forall st addr addr' v,
not_too_high addr
-> not_too_high addr'
-> apart addr addr'
-> get_mem32 (set_mem32 st addr v) addr' = get_mem32 st addr'.
Expression evaluation |
Definition eval_shift sop n1 n2 :=
match sop with
| Shl => bshl32 n1 n2
| Shr => bshr32 n1 n2
end.
Fixpoint evalExp (st : salState) (e : salExp) {struct e} : int32 :=
match e with
| SConst n => n
| SReg r => get_reg st r
| SArith aop e1 e2 => eval_arith aop (evalExp st e1) (evalExp st e2)
| SShift sop e n => eval_shift sop (evalExp st e) n
end.
Definition arith_flags st aop n1 n2 :=
Build_salState (SstRegs st) (arith_flags' (SstFlags st) aop n1 n2)
(SstMem st) (SstPc st).
Definition arith_flags_no_CF st aop n1 n2 :=
Build_salState (SstRegs st) (arith_flags_no_CF' (SstFlags st) aop n1 n2)
(SstMem st) (SstPc st).
Definition set_arith_flags cmp :=
match cmp with
| SWithCF => arith_flags
| SNoCF => arith_flags_no_CF
end.
Definition check_cc st cb := check_cc' (SstFlags st) cb.
Definition salExecCmd (st : salState) (cmd : salCmd) : salState :=
match cmd with
| SSet r e => set_reg st r (evalExp st e)
| SLoad r e => set_reg st r (get_mem32 st (evalExp st e))
| SStore e1 e2 => set_mem32 st (evalExp st e1) (evalExp st e2)
| SCompare cmp aop e1 e2 => set_arith_flags cmp st aop (evalExp st e1) (evalExp st e2)
end.
Definition salExecJmp (jmp : salJump) (nextPc : int32) (st : salState) : option salState :=
match jmp with
| SFail => None
| SFallthru => Some (set_pc st nextPc)
| SJump pc => Some (set_pc st pc)
| SIndirectJump _ e => Some (set_pc st (evalExp st e))
| SConditionalJump co pc =>
Some (if check_cc st co
then set_pc st pc
else set_pc st nextPc)
end.
Definition salExec' (insPc : salInstr * int32) (st : salState) : option salState :=
salExecJmp (snd (fst insPc)) (snd insPc) (fold_left salExecCmd (fst (fst insPc)) st).
Definition salAddr (addr : address) : salExp :=
let n := SConst (addrDisp addr) in
let n := match addrBase addr with
| None => n
| Some base => SArith Add n (SReg (SX86 base))
end in
match addrIndex addr with
| None => n
| Some (sc, idx) =>
SArith Add n (SShift Shl (SReg (SX86 idx)) (scale_shift sc))
end.
Definition salGenop (tmp : salReg) (gop : genop32) : list salCmd * salExp :=
match gop with
| Imm n => (nil, SConst n)
| Reg r => (nil, SReg (SX86 r))
| Address a => (cons (SLoad tmp (salAddr a)) nil, SReg tmp)
end.
Definition failureInstr : salInstr := (nil, SFail).
Definition salCompile insPc :=
match fst insPc with
| Arith aop (Reg r) g =>
let (loads, g') := salGenop STmp1 g in
(app loads
(cons (SCompare SWithCF aop (SReg (SX86 r)) g')
(cons (SSet (SX86 r) (SArith aop (SReg (SX86 r)) g'))
nil)), SFallthru)
| Arith aop (Address a) g =>
let (loads, g') := salGenop STmp2 g in
(app (cons (SLoad STmp1 (salAddr a)) loads)
(cons (SCompare SWithCF aop (SReg STmp1) g')
(cons (SStore (salAddr a) (SArith aop (SReg STmp1) g'))
nil)), SFallthru)
| Call g =>
let (loads, g') := salGenop STmp1 g in
(app (cons (SStore (SArith Add (SConst neg_four) (SReg (SX86 ESP))) (SConst (snd insPc)))
(cons (SSet (SX86 ESP) (SArith Sub (SReg (SX86 ESP)) (SConst four)))
nil)) loads,
SIndirectJump SCall g')
| Cmp g1 g2 =>
let (loads1, g1') := salGenop STmp1 g1 in
let (loads2, g2') := salGenop STmp2 g2 in
(app (app loads1 loads2) (cons (SCompare SWithCF Sub g1' g2') nil), SFallthru)
| Inc (Reg r) =>
(cons (SCompare SNoCF Add (SReg (SX86 r)) (SConst bone32))
(cons (SSet (SX86 r) (SArith Add (SReg (SX86 r)) (SConst bone32)))
nil), SFallthru)
| Inc (Address a) =>
(cons (SLoad STmp1 (salAddr a))
(cons (SCompare SNoCF Add (SReg STmp1) (SConst bone32))
(cons (SStore (salAddr a) (SArith Add (SReg STmp1) (SConst bone32)))
nil)), SFallthru)
| Jcc c pc =>
(nil, SConditionalJump c pc)
| Jmp pc =>
(nil, SJump pc)
| Lea r a =>
(cons (SSet (SX86 r) (salAddr a)) nil, SFallthru)
| Leave =>
(cons (SSet (SX86 ESP) (SArith Add (SConst four) (SReg (SX86 EBP))))
(cons (SLoad (SX86 EBP) (SReg (SX86 EBP)))
nil), SFallthru)
| Mov (Reg r) g =>
let (loads, g') := salGenop STmp1 g in
(app loads (cons (SSet (SX86 r) g') nil), SFallthru)
| Mov (Address a) g =>
let (loads, g') := salGenop STmp1 g in
(app loads (cons (SStore (salAddr a) g') nil), SFallthru)
| Pop (Reg r) =>
(cons (SLoad (SX86 r) (SReg (SX86 ESP)))
(cons (SSet (SX86 ESP) (SArith Add (SConst four) (SReg (SX86 ESP))))
nil), SFallthru)
| Pop (Address a) =>
(cons (SLoad STmp1 (SReg (SX86 ESP)))
(cons (SStore (salAddr a) (SReg STmp1))
(cons (SSet (SX86 ESP) (SArith Add (SConst four) (SReg (SX86 ESP))))
nil)), SFallthru)
| Push g =>
let (loads, g') := salGenop STmp1 g in
(app loads
(cons (SStore (SArith Add (SConst neg_four) (SReg (SX86 ESP))) g')
(cons (SSet (SX86 ESP) (SArith Add (SConst neg_four) (SReg (SX86 ESP))))
nil)), SFallthru)
| Ret =>
(cons (SLoad STmp1 (SReg (SX86 ESP)))
(cons (SSet (SX86 ESP) (SArith Add (SConst four) (SReg (SX86 ESP))))
nil), SIndirectJump SRet (SReg STmp1))
| _ => failureInstr
end.
Definition salInstruction := (instr * salInstr)%type.
Definition get_sal_instr st :=
let (ins, pc) := get_instr st in
((ins, salCompile (ins, pc)), pc).
Definition salExec (insPc : salInstruction * int32) (st st' : salState) :=
salExec' (snd (fst insPc), snd insPc) st = Some st'.
The SAL abstract machine |
| Concretization relation |
Record R (st : state) (st' : salState) : Prop := {
Rregs : forall r, get_reg st' (SX86 r) = get_reg32 st r;
Rflags : SstFlags st' = stFlags st;
Rmem : SstMem st' = stMem st;
Rpc : SstPc st' = stPc st
}.
Module Sal86 (Param : M86_PARAM) <: MACHINE.
Definition mstate := salState.
Definition minitState st := exists st', R st' st /\ Param.minitState st'.
Definition minstr := salInstruction.
Definition mget_instr := get_sal_instr.
Definition mexec := salExec.
End Sal86.
Relating SAL to X86 |
Module Make (Param : M86_PARAM).
Module MC := M86(Param).
Module M := Sal86(Param).
Module Checker (_Abs : ABSTRACTION with Module Mac := M)
: CHECKER with Module Mac := MC.
Module Reduction <: REDUCTION.
Definition cameFrom : forall (ins : instr * salInstr),
{ins' : instr
| forall abs nextPc, get_sal_instr abs = (ins, nextPc)
-> forall st, R st abs -> Defs.get_instr st = (ins', nextPc)}.
Definition liftState (st : state) :=
Build_salState
(SalRegMap.set (SX86 EAX) (get_reg32 st EAX)
(SalRegMap.set (SX86 ECX) (get_reg32 st ECX)
(SalRegMap.set (SX86 EDX) (get_reg32 st EDX)
(SalRegMap.set (SX86 EBX) (get_reg32 st EBX)
(SalRegMap.set (SX86 ESP) (get_reg32 st ESP)
(SalRegMap.set (SX86 EBP) (get_reg32 st EBP)
(SalRegMap.set (SX86 ESI) (get_reg32 st ESI)
(SalRegMap.set (SX86 EDI) (get_reg32 st EDI)
(SalRegMap.init bzero32)))))))))
(stFlags st) (stMem st) (stPc st).
Theorem init : forall conc, Param.minitState conc
-> exists abs, R conc abs /\ M.minitState abs.
Hint Constructors exec write_genop32.
Definition check_cc_eq : forall abs conc c,
R conc abs
-> check_cc abs c = Defs.check_cc conc c.
Definition check_cc_imp : forall abs conc c b,
R conc abs
-> check_cc abs c = b
-> Defs.check_cc conc c = b.
Hint Resolve check_cc_imp.
Definition check_cc_eq' : forall abs conc c,
SstFlags abs = stFlags conc
-> check_cc abs c = Defs.check_cc conc c.
Definition check_cc_imp' : forall abs conc c b,
SstFlags abs = stFlags conc
-> Defs.check_cc conc c = b
-> check_cc abs c = b.
Hint Rewrite check_cc_imp' using assumption : Maps.
Hint Rewrite SalRegMap.gss Reg32Map.gss : Maps.
Hint Rewrite SalRegMap.gso Reg32Map.gso using congruence : Maps.
Hint Unfold get_reg get_reg32 set_pc arith_flags.
Ltac unfold_get :=
match goal with
| [ H : forall r : reg32, get_reg _ _ = get_reg32 _ _ |- _ ] =>
unfold get_reg, get_reg32 in H; rewrite H; repeat rewrite H
end.
Ltac rewrite_get :=
match goal with
| [ H : forall r : reg32, get_reg _ _ = get_reg32 _ _ |- _ ] =>
rewrite H; repeat rewrite H
end.
Ltac get_cases :=
match goal with
| [ |- context[Reg32Map.get ?r0 (Reg32Map.set ?r _ _)] ] =>
destruct (reg32_eq_dec r0 r); subst; autorewrite with Maps
end.
Lemma eval_addr_reg : forall r conc,
eval_addr (Build_address bzero32 (Some r) None) conc
= get_reg32 conc r.
Hint Rewrite eval_addr_reg : Maps.
Lemma eval_addr_stack : forall r conc,
eval_addr (Build_address neg_four (Some r) None) conc
= badd32 neg_four (get_reg32 conc r).
Hint Rewrite eval_addr_stack : Maps.
Lemma evalExp_salAddr : forall conc abs a,
(forall r : reg32,
SalRegMap.get (SX86 r) (SstRegs abs) =
Reg32Map.get r (stRegs32 conc))
-> evalExp abs (salAddr a) = eval_addr a conc.
Definition compile : forall (insPc : instr * int32),
{ins' : salInstruction
| forall conc abs,
R conc abs
-> (forall abs', salExec (ins', snd insPc) abs abs'
-> exists conc', exec insPc conc conc')
/\ (forall conc', exec insPc conc conc'
-> exists abs', salExec (ins', snd insPc) abs abs'
/\ R conc' abs')}.
Definition R := R.
Module Conc := MC.
Module Abs := _Abs.
End Reduction.
Module Ch := Reduce.Make(Reduction).
Module Mac := MC.
Definition verify := Ch.verify.
End Checker.
End Make.