| Adding simple conditional branch consideration support to a type system |
Require Import Arith List TheoryList ZArith.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Tactics.
Require Import Asm.Util.ListUtil.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Util.Monad.
Require Import Asm.Util.Mod.
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.Sal.
Require Import ProofOS.AbsInt.FixedCode.
Require Import ProofOS.AbsInt.TypeSystem.
Require Import ProofOS.AbsInt.StackTypes.
Set Implicit Arguments.
Definition eval_test fg :=
match fg with
| CF => Some eval_CF
| PF => Some eval_PF
| AF => Some eval_AF
| ZF => Some eval_ZF
| SF => Some eval_SF
| OF => Some eval_OF
| _ => None
end.
Definition eval_condition' c aop e1 e2 :=
match c with
| O => eval_OF aop e1 e2
| B => eval_CF aop e1 e2
| Z => eval_ZF aop e1 e2
| BE => eval_CF aop e1 e2 || eval_ZF aop e1 e2
| S => eval_SF aop e1 e2
| P => eval_PF aop e1 e2
| L => negb (eqb (eval_SF aop e1 e2) (eval_OF aop e1 e2))
| LE => eval_ZF aop e1 e2 || negb (eqb (eval_SF aop e1 e2) (eval_OF aop e1 e2))
end.
Definition eval_cc c aop e1 e2 :=
eqb (eval_condition' (snd c) aop e1 e2) (fst c).
Section condTy.
Variable mastate : Set.
Record condState : Set := {
csFlags : FlagMap.t (option (arith_op * salExp * salExp));
csCust : mastate
}.
Parameter print_condState : (mastate -> unit)
-> ((flag * option (arith_op * salExp * salExp) -> unit) -> unit)
-> mastate -> unit.
End condTy.
Module Make (Param : M86_PARAM_FIXED_CODE_AND_STACK).
Module Stack := StackTypes.Make(Param).
Import Stack.
Import TySys.
Import Param.
Import Fixed.
Import MySal.
Section condTy2.
Variables mastate mcontext : Set.
Variable mconc : mcontext -> salState -> mastate -> Prop.
Record condConc (ctx : mcontext) (st : salState) (abs : condState mastate) : Prop := {
ccFlags : forall fg, match FlagMap.get fg (csFlags abs) with
| None => True
| Some (aop, e1, e2) =>
match eval_test fg with
| None => False
| Some eval_flag =>
FlagMap.get fg (SstFlags st)
= eval_flag aop (evalExp st e1) (evalExp st e2)
end
end;
ccCust : mconc ctx st (csCust abs)
}.
End condTy2.
Module Type TYPE_SYSTEM_WITH_TESTING.
Declare Module Sys : STACK_READY_TYPE_SYSTEM.
Parameter considerTest : forall (abs : stateDescription (stackTy Sys.ty)
(stackState Sys.ty Sys.mastate))
(co : cc) (aop : arith_op) (e1 e2 : salExp) (b : bool),
{abs' : _
| forall ctx st,
typeMconc (stackHasTy Sys.hasTy) (stackConc Sys.hasTy Sys.mconc) ctx st abs
-> eval_cc co aop (evalExp st e1) (evalExp st e2) = b
-> typeMconc (stackHasTy Sys.hasTy) (stackConc Sys.hasTy Sys.mconc) ctx st abs'}.
End TYPE_SYSTEM_WITH_TESTING.
Add conditional testing support to a type system |
Module AddCond (SysPlus : TYPE_SYSTEM_WITH_TESTING) : STACK_READY_TYPE_SYSTEM
with Definition ty := SysPlus.Sys.ty
with Definition mastate := condState SysPlus.Sys.mastate
with Definition mcontext := SysPlus.Sys.mcontext
with Definition hasTy := SysPlus.Sys.hasTy
with Definition mconc := condConc SysPlus.Sys.mconc.
Module Mac := M.
Import SysPlus.
Import Sys.
Definition ty := ty.
Definition print_ty := print_ty.
Definition mastate := condState mastate.
Definition print_mastate ss :=
let (default, elems) := FlagMap.elements (csFlags ss) in
print_condState print_mastate
(fun f => iter f elems) (csCust ss).
Definition mcontext := mcontext.
Definition hasTy := hasTy.
Hint Unfold hasTy.
Definition mconc := condConc mconc.
Hint Unfold mconc.
Hint Constructors condConc.
Definition subTy := subTy.
Definition arith_op_eq_dec : forall (x y : arith_op), {x = y} + {x <> y}.
Definition shift_op_eq_dec : forall (x y : shift_op), {x = y} + {x <> y}.
Definition salExp_eq_dec : forall (x y : salExp), {x = y} + {x <> y}.
Definition eq_dec_triple : forall (x y : arith_op * salExp * salExp), {x = y} + {x <> y}.
Definition eq_dec_tripleOpt : forall (x y : option (arith_op * salExp * salExp)), {x = y} + {x <> y}.
Definition tripleOpt_ok (x y : option (arith_op * salExp * salExp)) :=
x = y \/ y = None.
Definition check_tripleOpt : forall (x y : option (arith_op * salExp * salExp)),
pred_option (tripleOpt_ok x y).
Definition subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
Definition tyTop := tyTop.
Definition tyTopSound := tyTopSound.
Definition tyConst := tyConst.
Definition isTyConst := isTyConst.
Definition tyConstSound1 := tyConstSound1.
Definition tyConstSound2 := tyConstSound2.
Definition typeof : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
{t : ty
| forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> hasTy ctx (evalExp st e) t}.
Definition typeofLoad : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
{t : ty
| forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> hasTy ctx (get_mem32 st (evalExp st e)) t}.
Definition checkStore : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
pred_option (forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> apartFromCode (evalExp st e)
/\ not_too_high (evalExp st e)
/\ apartFromStack (evalExp st e)).
Definition expUnaffected : forall (cmd : salCmd) (e : salExp),
pred_option (forall st, evalExp st e = evalExp (salExecCmd st cmd) e).
Lemma evalExp_flags : forall e st fls,
evalExp (Build_salState (SstRegs st) fls (SstMem st) (SstPc st)) e
= evalExp st e.
Hint Rewrite FlagMap.gss : Maps.
Hint Rewrite FlagMap.gso using (auto; discriminate) : Maps.
Definition effectOfCmd : forall (abs : mastate) (rs : SalRegMap.t ty) (cmd : salCmd),
sig_option (fun abs' => forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> mconc ctx (salExecCmd st cmd) abs').
Lemma evalExp_mem : forall e st pc a v,
evalExp (Build_salState (SstRegs st) (SstFlags st) (set_mem32' (SstMem st) a v) pc) e
= evalExp st e.
Definition doStackWrite : forall (abs : mastate),
sig_option (fun abs' => forall ctx st dst src,
mconc ctx st abs
-> inStack dst
-> mconc ctx (set_mem32 st dst src) abs').
Lemma evalExp_pc : forall e st pc,
evalExp (Build_salState (SstRegs st) (SstFlags st) (SstMem st) pc) e
= evalExp st e.
Definition effectOfJump : forall (abs : mastate) (rs : SalRegMap.t ty)
(jmp : salJump) (nextPc : int32),
sig_option (fun abs' => forall ctx st,
mconc ctx st abs
-> (forall r, hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> match salExecJmp jmp nextPc st with
| None => False
| Some st' => mconc ctx st' abs'
end).
Definition absEval_cc : forall (abs : mastate) (co : cc),
sig_option (fun triple => forall ctx st,
mconc ctx st abs
-> check_cc st co = eval_cc co (fst (fst triple))
(evalExp st (snd (fst triple)))
(evalExp st (snd triple))).
Definition effectOfConditionalJump : forall (abs : stateDescription (stackTy ty)
(stackState ty mastate))
(co : cc) (pc nextPc : int32) (b : bool),
sig_option (fun abs' => forall ctx st,
typeMconc (stackHasTy hasTy) (stackConc hasTy mconc) ctx st abs
-> check_cc st co = b
-> match salExecJmp (SConditionalJump co pc) nextPc st with
| None => False
| Some st' => typeMconc (stackHasTy hasTy) (stackConc hasTy mconc) ctx st' abs'
end).
Definition viewShiftOfJump : forall (hyps : list (stateDescription ty mastate))
(abs : stateDescription ty mastate)
(jmp : salJump) (nextPc : int32),
sig_option (fun vs => forall ctx st,
typeMconc hasTy mconc ctx st abs
-> exists ctx', typeMconc hasTy mconc ctx' st (vsAbs vs)
/\ AllS (fun need => exists have, (In have (vsSuccs vs) \/ In have hyps)
/\ subsumes (typeMconc hasTy mconc) ctx' need ctx have) (vsHyps vs)).
End AddCond.
End Make.