| Adding simple stack 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.
Set Implicit Arguments.
Maps used in abstract state |
Module NatIndexed <: INDEXED_TYPE.
Definition t := nat.
Definition index := P_of_succ_nat.
Theorem index_inj: forall (x y: t), index x = index y -> x = y.
Definition eq := eq_nat_dec.
Definition invert n := pred (nat_of_P n).
Theorem invert_index : forall x, invert (index x) = x.
End NatIndexed.
Module NatMap := IMap(NatIndexed).
Definition disjointRegions (start1 : int32) len1 (start2 : int32) len2 :=
bvec_to_nat start1 + len1 + 4 <= bvec_to_nat start2
\/ bvec_to_nat start1 >= bvec_to_nat start2 + len2 + 4.
Module Type M86_PARAM_FIXED_CODE_AND_STACK.
Parameter minitState : state -> Prop.
Parameter minitMem : mem.
Parameter codeStart : int32.
Parameter codeLength : nat.
Axiom codeHigh : bvec_to_nat codeStart >= 4.
Axiom codeFits : bvec_to_nat codeStart + codeLength < pow2 32 - 3.
Axiom pcInRange : forall st, minitState st
-> bvec_to_nat codeStart
<= bvec_to_nat (stPc st)
< bvec_to_nat codeStart + codeLength - longestInstr.
Axiom codeUniform : forall st, minitState st
-> agree_range (stMem st) minitMem codeStart codeLength.
Parameter stackStart : int32.
Parameter stackLength : nat.
Axiom stackHigh : bvec_to_nat stackStart >= 4.
Axiom stackFits : bvec_to_nat stackStart + stackLength < pow2 32 - 3.
Axiom stackCodeSeparate : disjointRegions codeStart codeLength stackStart stackLength.
End M86_PARAM_FIXED_CODE_AND_STACK.
Metadata types |
Section metadata.
Variable ty : Set.
Record function_info : Set := {
fiPc : int32;
| First program counter |
fiRet : ty;
| Return type |
fiArgs : list ty
| How many arguments? |
}.
End metadata.
Section stackTy.
Variables ty mastate : Set.
Inductive stackTy : Set :=
| Top
| Const : int32 -> stackTy
| Stack : nat -> stackTy
| OldEbp : stackTy
| RetPtr : stackTy
| Cust : ty -> stackTy.
Parameter print_stackTy : (ty -> unit) -> stackTy -> unit.
Record stackState : Set := {
aIsRet : bool;
aStackSize : nat;
aStackSlots : NatMap.t stackTy;
aCustom : mastate
}.
Parameter print_stackState : (ty -> unit) -> (mastate -> unit)
-> nat -> stackTy -> ((nat * stackTy -> unit) -> unit) -> mastate -> unit.
End stackTy.
Module Make (Param : M86_PARAM_FIXED_CODE_AND_STACK).
Module TySys := TypeSystem.Make(Param).
Import TySys.
Import Param.
Import Fixed.
Import MySal.
Definition stackEnd := nat_to_bvec 32 (bvec_to_nat stackStart + stackLength).
Definition inStack (a : int32) :=
bvec_to_nat stackStart <= bvec_to_nat a <= bvec_to_nat stackStart + stackLength.
Definition apartFromStack (a : int32) :=
bvec_to_nat a <= bvec_to_nat stackStart - 4
\/ bvec_to_nat a >= bvec_to_nat stackStart + stackLength + 4.
The language of types used in basic block preconditions for outputs ofthis functor |
Section stackTy2.
Variables ty mastate mcontext : Set.
Variable hasTy : mcontext -> int32 -> ty -> Prop.
Variable mconc : mcontext -> M.mstate -> mastate -> Prop.
Record stackContext : Set := {
ctxSptr : int32;
ctxMemIn : mem;
ctxOldEbp : int32;
ctxRetPtr : option int32;
ctxCust : mcontext
}.
Definition stack_slot (ctx : stackContext) n :=
nat_to_bvec 32 (bvec_to_nat (ctxSptr ctx) - n).
Inductive stackHasTy : stackContext -> int32 -> stackTy ty -> Prop :=
| HT_Top : forall ctx v, stackHasTy ctx v (Top _)
| HT_Const : forall ctx v, stackHasTy ctx v (Const _ v)
| HT_Stack : forall ctx n,
n <= bvec_to_nat (ctxSptr ctx)
-> stackHasTy ctx (stack_slot ctx n) (Stack _ n)
| HT_OldEbp : forall ctx, stackHasTy ctx (ctxOldEbp ctx) (OldEbp _)
| HT_RetPtr : forall ctx r, ctxRetPtr ctx = Some r
-> stackHasTy ctx r (RetPtr _)
| HT_Cust : forall ctx v t, hasTy (ctxCust ctx) v t
-> stackHasTy ctx v (Cust t).
Definition conc_slots ctx st (abs : stackState ty mastate) :=
forall n, 4 <= n < aStackSize abs
-> stackHasTy ctx (get_mem32 st (stack_slot ctx n)) (NatMap.get n (aStackSlots abs)).
Definition agree_range' (mem1 mem2 : mem) (addr1 addr2 : int32) :=
forall addr', bvec_to_nat addr1 <= bvec_to_nat addr' < bvec_to_nat addr2
-> Int32Map.get addr' mem1 = Int32Map.get addr' mem2.
Record stackConc (ctx : stackContext) (st : M.mstate) (abs : stackState ty mastate) : Prop := {
mcPc : aIsRet abs = true -> ctxRetPtr ctx = Some (SstPc st);
mcSptr : bvec_to_nat (ctxSptr ctx) <= bvec_to_nat stackStart + stackLength - 4;
mcStackSize : bvec_to_nat stackStart + aStackSize abs < bvec_to_nat (ctxSptr ctx);
mcStackSlots : conc_slots ctx st abs;
mcMemIn : agree_range' (SstMem st) (ctxMemIn ctx) (ctxSptr ctx) stackEnd;
mcCust : mconc (ctxCust ctx) st (aCustom abs)
}.
Lemma ntb_cong : forall len n1 n2,
n1 = n2
-> nat_to_bvec len n1 = nat_to_bvec len n2.
Definition stackSlotOf : forall (abs : stateDescription (stackTy ty) (stackState ty mastate)) (e : salExp),
sig_option (fun ss => forall ctx st,
typeMconc stackHasTy stackConc ctx st abs
-> evalExp st e = stack_slot ctx ss).
End stackTy2.
Module Type STACK_READY_TYPE_SYSTEM.
Parameter ty : Set.
Parameter print_ty : ty -> unit.
| A language of types describing machine words |
Parameter mastate : Set.
Parameter print_mastate : mastate -> unit.
| Custom abstract state information |
Parameter mcontext : Set.
| A summary of aspects of a machine state that don't need to be represented explicitly at verification time, but are important in soundness proofs |
Parameter mconc : mcontext -> M.mstate -> mastate -> Prop.
| Concretization relation |
Parameter subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
| A way to check compatibility of abstract states |
Parameter hasTy : mcontext -> int32 -> ty -> Prop.
| What it means for a word to be of a type |
Parameter tyTop : ty.
Axiom tyTopSound : forall ctx v, hasTy ctx v tyTop.
Parameter tyConst : int32 -> ty.
Axiom tyConstSound1 : forall ctx v, hasTy ctx v (tyConst v).
Axiom tyConstSound2 : forall ctx v1 v2, hasTy ctx v1 (tyConst v2) -> v1 = v2.
Parameter isTyConst : forall (t : ty), sig_option (fun n => t = tyConst n).
Parameter subTy : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
| A way to check compatibility of types |
Parameter 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}.
| A type inference procedure for SAL expressions |
Parameter 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}.
| Type inference for memory loads |
Parameter 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)).
| Type inference for memory loads |
Parameter 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').
| Update the custom state to reflect the result of a command. |
Parameter 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').
| The custom type system should be unaffected by stack writes. |
Parameter 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).
| Update the custom state to reflect the result of a jump. |
Parameter 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).
Specialized version of effectOfJump that allows different states in
different cases of a conditional jump test
|
Parameter 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)).
| Massage the form of an abstract state to match what a jump target expects; for instance, at a function call. |
End STACK_READY_TYPE_SYSTEM.
Module Type TYPE_SYSTEM_WITH_FUNCTIONS.
Declare Module Sys : STACK_READY_TYPE_SYSTEM.
Parameter functions : list (function_info (stackTy Sys.ty)).
| Information on function types |
End TYPE_SYSTEM_WITH_FUNCTIONS.
Add stack support to a type system |
Module AddStackTypes (SysPlus : TYPE_SYSTEM_WITH_FUNCTIONS) : TYPE_SYSTEM
with Definition ty := stackTy SysPlus.Sys.ty
with Definition mastate := stackState SysPlus.Sys.ty SysPlus.Sys.mastate
with Definition mcontext := stackContext SysPlus.Sys.mcontext
with Definition hasTy := stackHasTy SysPlus.Sys.hasTy
with Definition mconc := stackConc SysPlus.Sys.hasTy SysPlus.Sys.mconc.
Module Mac := M.
Import SysPlus.
Import Sys.
Definition ty := stackTy ty.
Definition print_ty := print_stackTy print_ty.
Definition mastate := stackState Sys.ty mastate.
Definition print_mastate ss :=
let (default, elems) := NatMap.elements (aStackSlots ss) in
print_stackState Sys.print_ty print_mastate
(aStackSize ss) default (fun f => iter f elems) (aCustom ss).
Definition mcontext := stackContext mcontext.
Definition hasTy := stackHasTy hasTy.
Hint Unfold hasTy.
Hint Constructors stackHasTy.
Definition mconc := stackConc Sys.hasTy mconc.
Hint Unfold mconc.
Hint Constructors stackConc.
Hint Resolve tyConstSound1 tyConstSound2.
Lemma HT_Const' : forall ctx v1 v2,
v1 = v2
-> hasTy ctx v1 (Const _ v2).
Hint Resolve HT_Const'.
Definition subTy : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
Definition bool_eq_dec : forall (x y : bool), {x = y} + {x <> y}.
Definition subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
Lemma mconc_sptr_not_too_high : forall ctx st abs,
mconc ctx st abs
-> not_too_high (ctxSptr ctx).
Hint Resolve mconc_sptr_not_too_high.
Lemma not_too_high_minus : forall n1 n2,
not_too_high n1
-> bvec_to_nat n1 - n2 < pow2 32.
Hint Resolve not_too_high_minus.
Lemma stack_slot_rewrite : forall ctx st abs n1 n2,
mconc ctx st abs
-> n1 <= bvec_to_nat (ctxSptr ctx)
-> bvec_to_nat n2 <= n1
-> badd32 (stack_slot ctx n1) n2
= stack_slot ctx (n1 - bvec_to_nat n2).
Lemma stack_slot_rewrite2 : forall ctx st abs n1 n2,
mconc ctx st abs
-> n1 <= bvec_to_nat (ctxSptr ctx)
-> n1 + bvec_to_nat n2 <= aStackSize abs
-> bsub32 (stack_slot ctx n1) n2
= stack_slot ctx (n1 + bvec_to_nat n2).
Lemma stack_slot_rewrite3 : forall (ctx : mcontext) st (abs : mastate) n1 n2,
mconc ctx st abs
-> n1 < bvec_to_nat n2
-> n1 + bvec_to_nat (bneg n2) <= aStackSize abs
-> n1 <= bvec_to_nat (ctxSptr ctx)
-> badd32 n2 (stack_slot ctx n1)
= stack_slot ctx (n1 + bvec_to_nat (bneg n2)).
Definition lowerTy t :=
match t with
| Const n => tyConst n
| Cust t' => t'
| _ => tyTop
end.
Hint Resolve tyTopSound.
Lemma lowerTy_sound : forall st r ctx t,
hasTy ctx (get_reg st r) t
-> Sys.hasTy (ctxCust ctx) (get_reg st r) (lowerTy t).
Hint Resolve lowerTy_sound.
Definition typeofR (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 raiseTy : forall (t : Sys.ty), {t' : ty |
forall ctx v, Sys.hasTy (ctxCust ctx) v t -> hasTy ctx v t'}.
Lemma lowerTy_map_sound : forall ctx st rs,
(forall r : SalRegIndexed.t,
hasTy ctx (get_reg st r) (SalRegMap.get r rs))
-> (forall r : SalRegIndexed.t,
Sys.hasTy (ctxCust ctx) (get_reg st r)
(SalRegMap.get r (SalRegMap.map lowerTy rs))).
Hint Resolve lowerTy_map_sound.
Definition typeof : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
typeofR abs rs e.
Definition typeofLoadR (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 typeofLoad : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
typeofLoadR abs rs e.
Lemma apartFromCode_slot : forall (ctx : mcontext) (abs : mastate) n,
bvec_to_nat (ctxSptr ctx) <= bvec_to_nat stackStart + stackLength - 4
-> bvec_to_nat stackStart + aStackSize abs < bvec_to_nat (ctxSptr ctx)
-> n <= bvec_to_nat (ctxSptr ctx)
-> n < aStackSize abs
-> apartFromCode (stack_slot ctx n).
Hint Resolve apartFromCode_slot.
Lemma not_too_high_slot : forall n (ctx : mcontext),
bvec_to_nat (ctxSptr ctx) <= bvec_to_nat stackStart + stackLength - 4
-> n <= bvec_to_nat (ctxSptr ctx)
-> not_too_high (stack_slot ctx n).
Hint Resolve not_too_high_slot.
Definition checkStoreR (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)).
Definition checkStore : forall (abs : mastate) (rs : SalRegMap.t ty) (e : salExp),
checkStoreR abs rs e.
Definition set_stack32 (m : NatMap.t ty) n t :=
NatMap.set (n-3) (Top _)
(NatMap.set (n-2) (Top _)
(NatMap.set (n-1) (Top _)
(NatMap.set (n+1) (Top _)
(NatMap.set (n+2) (Top _)
(NatMap.set (n+3) (Top _)
(NatMap.set n t m)))))).
Hint Rewrite NatMap.gss : Maps.
Hint Rewrite NatMap.gso using (trivial; fail) : Maps.
Lemma set_stack32_sound : forall (ctx : mcontext) st (abs : mastate) src tSrc n (cust : Sys.mastate),
bvec_to_nat stackStart + aStackSize abs < bvec_to_nat (ctxSptr ctx)
-> bvec_to_nat (ctxSptr ctx) <= bvec_to_nat stackStart + stackLength - 4
-> conc_slots Sys.hasTy ctx st abs
-> hasTy ctx src tSrc
-> n < aStackSize abs
-> conc_slots Sys.hasTy ctx (set_mem32 st (stack_slot ctx n) src)
(Build_stackState (aIsRet abs) (aStackSize abs)
(set_stack32 (aStackSlots abs) n tSrc) cust).
Hint Resolve set_stack32_sound.
Lemma agree_range'_write : forall m1 m2 a1 a2 a v,
agree_range' m1 m2 a1 a2
-> bvec_to_nat a + 4 <= bvec_to_nat a1
-> not_too_high a
-> agree_range' (set_mem32' m1 a v) m2 a1 a2.
Hint Resolve agree_range'_write.
Ltac use_gmap :=
match goal with
| [ |- context[SalRegMap.get _ (SalRegMap.map _ _)] ] =>
rewrite SalRegMap.gmap
end.
Hint Extern 1 (Sys.hasTy _ _ _) => use_gmap.
Lemma apartFromStack_heap_write : forall dst ctx st (abs : mastate) src (cust : Sys.mastate),
apartFromStack dst
-> not_too_high dst
-> bvec_to_nat (ctxSptr ctx) <= bvec_to_nat stackStart + stackLength - 4
-> bvec_to_nat stackStart + aStackSize abs < bvec_to_nat (ctxSptr ctx)
-> conc_slots Sys.hasTy ctx st abs
-> conc_slots Sys.hasTy ctx (set_mem32 st dst src)
(Build_stackState (aIsRet abs) (aStackSize abs) (aStackSlots abs) cust).
Lemma apartFromStack_agree_range' : forall dst m1 m2 src sptr ssize,
not_too_high dst
-> apartFromStack dst
-> bvec_to_nat sptr <= bvec_to_nat stackStart + stackLength - 4
-> bvec_to_nat stackStart + ssize < bvec_to_nat sptr
-> agree_range' m1 m2 sptr stackEnd
-> agree_range' (set_mem32' m1 dst src) m2 sptr stackEnd.
Definition effectOfCmdR (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').
Definition effectOfCmd : forall (abs : mastate) (rs : SalRegMap.t ty) (cmd : salCmd),
effectOfCmdR abs rs cmd.
Definition effectOfJumpR (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 effectOfJump : forall (abs : mastate) (rs : SalRegMap.t ty)
(jmp : salJump) (nextPc : int32),
effectOfJumpR abs rs jmp nextPc.
Definition effectOfConditionalJump : forall (abs : stateDescription ty mastate)
(co : cc) (pc nextPc : int32) (b : bool),
sig_option (fun abs' => forall ctx st,
typeMconc hasTy mconc ctx st abs
-> check_cc st co = b
-> match salExecJmp (SConditionalJump co pc) nextPc st with
| None => False
| Some st' => typeMconc hasTy mconc ctx st' abs'
end).
Definition tyTop : ty := Top _.
Theorem tyTopSound : forall ctx v, hasTy ctx v tyTop.
Definition tyConst (n : int32) : ty := Const _ n.
Hint Unfold tyConst.
Theorem tyConstSound1 : forall ctx v, hasTy ctx v (tyConst v).
Theorem tyConstSound2 : forall ctx v1 v2, hasTy ctx v1 (tyConst v2) -> v1 = v2.
Definition isTyConst : forall (t : ty), sig_option (fun n => t = tyConst n).
Lemma agree_range'_refl : forall m a1 a2,
agree_range' m m a1 a2.
Hint Resolve agree_range'_refl.
Definition shiftContext (args : list ty) (ctx : mcontext) (st : salState) ss oldebp retptr :=
Build_stackContext
(stack_slot ctx (ss - 4 - 4 * length args))
(SstMem st)
oldebp
retptr
(ctxCust ctx).
Fixpoint argsStack (args : list ty) : NatMap.t ty :=
match args with
| nil => NatMap.init (Top _)
| cons t rest => NatMap.set (4 * length args) t (argsStack rest)
end.
Lemma undo_rewrite_fourx : forall n,
n + (n + (n + (n + 0))) = 4 * n.
Import Datatypes.
Lemma undo_rewrite_fourx_plus : forall n,
S (n + (S (n + S (n + (S (n + 0)))))) = 4 * (S n).
Hint Rewrite undo_rewrite_fourx undo_rewrite_fourx_plus : fixup.
Ltac mysimpl := simpl; autorewrite with fixup.
Ltac clear_one :=
match goal with
[ H : _ |- _ ] => clear H
end.
Ltac clear_all := repeat clear_one.
Definition robustType : forall (t : ty),
pred_option (forall ctx v, hasTy ctx v t
-> forall args st ss oldebp retptr, hasTy (shiftContext args ctx st ss oldebp retptr) v t).
Lemma checkArgs_add : forall n1 n2 n3 n4 n5,
n1 <= n2
-> n3 + n2 <= n4
-> n2 <= n4 - n3
-> n5 - (n4 - n3 - n1) = n5 - (n4 - n3 - n2) - (n2 - n1).
Definition checkArgsR (args args' : list ty) (slots : NatMap.t ty) ssize ss :=
sig_option (fun slots' => forall ctx st,
bvec_to_nat (ctxSptr ctx) <= bvec_to_nat stackStart + stackLength
-> (forall n, 4 <= n < ssize
-> hasTy ctx (get_mem32 st (stack_slot ctx n)) (NatMap.get n slots))
-> forall oldebp retptr,
forall n, 4 <= n < ssize - (ss - 4 - 4 * length args)
-> hasTy (shiftContext args ctx st ss oldebp retptr) (get_mem32 st
(stack_slot (shiftContext args ctx st ss oldebp retptr) n)) (NatMap.get n slots')).
Definition checkArgs' : forall (args args' : list ty) (Hargs : length args' <= length args)
(slots : NatMap.t ty) ssize ss,
4 <= ss - 4 * length args' /\ ss < ssize /\ 4 + 4 * length args <= ss
-> checkArgsR args args' slots ssize ss.
Definition checkArgs : forall (args : list ty) (slots : NatMap.t ty) ssize ss,
4 <= ss - 4 * length args /\ ss < ssize /\ 4 + 4 * length args <= ss
-> checkArgsR args args slots ssize ss.
Lemma shiftAbs_lt' : forall n1 n2 ss,
n1 < n2
-> ss < n1
-> ss < n2
-> n1 - ss < n2 - ss.
Lemma shiftAbs_lt'' : forall n1 n2 n3,
n3 < n2
-> n1 + n2 - n3 = n1 + (n2 - n3).
Lemma shiftAbs_lt : forall start size sptr ss n1 n2,
start + size < sptr
-> ss < size
-> start +
(size - (ss - n1 - n2)) <
sptr - (ss - n1 - n2).
Lemma rewrite_plus_four : forall n,
S (S (S (S n))) = 4 + n.
Lemma HT_Stack' : forall ctx n v,
n <= bvec_to_nat (ctxSptr ctx)
-> v = stack_slot ctx n
-> hasTy ctx v (Stack _ n).
Lemma Some_get_mem32_cong : forall st e e',
e = e'
-> Some (get_mem32 st e) = Some (get_mem32 st e').
Lemma viewShift_eq : forall ss size sptr n1 n2,
ss <= size
-> n1 + n2 <= ss
-> sptr - (ss - n1 - n2) - (n1 + n2) = sptr - ss.
Definition shiftAbs : forall (fi : function_info ty) ss (abs : mastate),
sig_option (fun abs' => forall ctx st oldebp,
mconc ctx st abs
-> mconc (shiftContext (fiArgs fi) ctx st ss oldebp
(Some (get_mem32 st (stack_slot ctx ss)))) st abs').
We build up a fast look-up structure to find function informationfrom program counters. |
Definition pcToFi_map' (fis : list (function_info ty)) m :=
fold_left (fun m fi => Int32Map.set (fiPc fi) (Some fi) m) fis m.
Definition pcToFi_map := pcToFi_map' functions (Int32Map.init None).
Definition pcToFi pc := Int32Map.get pc pcToFi_map.
Lemma viewShift_boring : forall abs hyps,
forall (ctx : stackContext Sys.mcontext) (st : salState),
typeMconc hasTy mconc ctx st abs ->
exists ctx' : stackContext Sys.mcontext,
typeMconc hasTy mconc ctx' st abs /\
AllS
(fun
need : stateDescription (stackTy Sys.ty)
(stackState Sys.ty Sys.mastate) =>
exists
have : stateDescription (stackTy Sys.ty)
(stackState Sys.ty Sys.mastate),
(False \/ In have hyps) /\
subsumes (typeMconc hasTy mconc) ctx' need ctx have) hyps.
Hint Resolve viewShift_boring.
Fixpoint preserveSlots (sl : nat) (slots : NatMap.t ty) {struct sl} : NatMap.t ty :=
match sl with
| O => NatMap.init (Top _)
| S sl' => NatMap.set sl' (NatMap.get sl' slots) (preserveSlots sl' slots)
end.
Definition reverseRobustType : forall (t : ty),
pred_option (forall ctx v args st ss oldebp retptr, hasTy (shiftContext args ctx st ss oldebp retptr) v t
-> hasTy ctx v t).
Lemma viewShift_ret_eq : forall n1 n2 n3 n4,
n2 <= n1
-> n3 + n4 <= n2
-> n1 - (n2 - n3 - n4) - n4 = n1 - (n2 - n3).
Lemma agree_range'_slot : forall m1 m2 bound finish a,
belowMax finish 3
-> agree_range' m1 m2 bound finish
-> bvec_to_nat bound <= bvec_to_nat a < bvec_to_nat finish - 3
-> get_mem32' m2 a = get_mem32' m1 a.
Lemma minus_lt : forall n m o,
n < m - 0
-> n - o < m.
Lemma minus_lt2 : forall n m o p,
n - m <= o < p
-> n - S m <= o < p.
Lemma agree_range'_S : forall m1 m2 (ctx : mcontext) bound finish,
belowMax (ctxSptr ctx) 0
-> agree_range' m1 m2 (stack_slot ctx (S bound)) finish
-> agree_range' m1 m2 (stack_slot ctx bound) finish.
Lemma belowMax_stackEnd : forall (n : int32),
bvec_to_nat n < bvec_to_nat stackEnd - 3
-> belowMax n 0.
Hint Resolve belowMax_stackEnd.
Lemma bound_sptr : forall sptr bound,
sptr < bvec_to_nat stackEnd - 3
-> sptr - bound < pow2 32.
Hint Resolve bound_sptr.
Lemma agree_range'_weaken : forall m1 m2 s1 s2 e,
agree_range' m1 m2 s1 e
-> bvec_to_nat s1 <= bvec_to_nat s2
-> agree_range' m1 m2 s2 e.
Lemma viewShift_concSlots : forall ctx ssize st st' bound slots,
bvec_to_nat (ctxSptr ctx) < bvec_to_nat stackEnd - 3
-> agree_range' (SstMem st') (SstMem st) (stack_slot ctx (bound - 1)) stackEnd
-> (forall n,
4 <= n < ssize ->
stackHasTy Sys.hasTy ctx (get_mem32 st (stack_slot ctx n))
(NatMap.get n slots))
-> forall n,
4 <= n < ssize ->
stackHasTy Sys.hasTy ctx (get_mem32 st' (stack_slot ctx n))
(NatMap.get n
(preserveSlots bound slots)).
Lemma agree_range'_trans : forall m1 m2 m3 s e,
agree_range' m1 m2 s e
-> agree_range' m2 m3 s e
-> agree_range' m1 m3 s e.
Definition viewShift_ret : forall (fi : function_info ty)
(abs : stateDescription ty mastate) ss rp,
ss <= aStackSize (sdCust abs)
-> 4 + 4 * length (fiArgs fi) <= ss
-> sig_option (fun retAbss => forall ctx st,
typeMconc hasTy mconc ctx st abs
-> subsumes (typeMconc hasTy mconc)
(shiftContext (fiArgs fi) ctx st ss (get_reg st (SX86 EBP))
(Some rp)) (fst retAbss)
ctx (snd retAbss)).
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 AddStackTypes.
End Make.