| Simplified construction of a type system involving memory accesses |
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.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.
Require Import ProofOS.AbsInt.SimpleCond.
Set Implicit Arguments.
Definition of a simple type system |
Module Type WEAK_UPDATE_TYPE_SYSTEM.
Parameter ty : Set.
Parameter print_ty : ty -> unit.
Parameter hasTy : (int32 -> option ty) -> int32 -> ty -> Prop.
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).
Parameter typeofArith : forall (aop : arith_op) (t1 t2 : ty),
{t : ty
| forall ctx v1 v2,
hasTy ctx v1 t1
-> hasTy ctx v2 t2
-> hasTy ctx (eval_arith aop v1 v2) t}.
Parameter typeofCell : forall (t : ty),
sig_option (fun t' =>
forall ctx v,
hasTy ctx v t
-> ctx v = Some t').
Parameter considerNeq : forall (t : ty) (v : int32),
{t' : ty
| forall ctx v1,
hasTy ctx v1 t
-> v1 <> v
-> hasTy ctx v1 t'}.
Parameter considerDerefEq : forall (t : ty) (v : int32),
{t' : ty
| forall ctx st v1,
(forall a,
match ctx a with
| None => True
| Some t2 => hasTy ctx (get_mem32 st a) t2
end)
-> hasTy ctx v1 t
-> get_mem32 st v1 = v
-> hasTy ctx v1 t'}.
Parameter considerDerefNeq : forall (t : ty) (v : int32),
{t' : ty
| forall ctx st v1,
(forall a,
match ctx a with
| None => True
| Some t2 => hasTy ctx (get_mem32 st a) t2
end)
-> hasTy ctx v1 t
-> get_mem32 st v1 <> v
-> hasTy ctx v1 t'}.
End WEAK_UPDATE_TYPE_SYSTEM.
Definition wordAligned (n : int32) := exists k, bvec_to_nat n = 4 * k.
Lemma wordAligned_neq : forall a1 a2,
a1 <> a2
-> wordAligned a1
-> wordAligned a2
-> apart a1 a2.
Hint Resolve wordAligned_neq.
Module Type M86_PARAM_FIXED_CODE_AND_STACK_AND_HEAP.
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.
Parameter heapStart : int32.
Parameter heapLength : nat.
Axiom heapHigh : bvec_to_nat heapStart >= 4.
Axiom heapFits : bvec_to_nat heapStart + heapLength < pow2 32 - 3.
Axiom heapCodeSeparate : disjointRegions codeStart codeLength heapStart heapLength.
Axiom heapStackSeparate : disjointRegions stackStart stackLength heapStart heapLength.
End M86_PARAM_FIXED_CODE_AND_STACK_AND_HEAP.
Definition weakState := SalRegMap.t (option salExp).
| Map each register to a possible expression whose dereference it is known to contain |
Parameter print_weakState : ((salReg * option salExp -> unit) -> unit) -> unit.
Module Make (Param : M86_PARAM_FIXED_CODE_AND_STACK_AND_HEAP).
Module Cond := SimpleCond.Make(Param).
Import Cond.
Import Stack.
Import TySys.
Import Fixed.
Import MySal.
Import Param.
Definition inHeap (addr : int32) :=
bvec_to_nat heapStart
<= bvec_to_nat addr
< bvec_to_nat heapStart + heapLength - 3.
Section weakTy2.
Variable ty : Set.
Variable hasTy : (int32 -> option ty) -> int32 -> ty -> Prop.
Definition concAddr (ctx : int32 -> option ty) (st : salState) (addr : int32) :=
match ctx addr with
| None => True
| Some t =>
wordAligned addr
/\ inHeap addr
/\ hasTy ctx (get_mem32 st addr) t
end.
Definition concReg (st : salState) (ws : weakState) (r : salReg) :=
match SalRegMap.get r ws with
| None => True
| Some e => get_reg st r = get_mem32 st (evalExp st e)
end.
Record weakConc (ctx : int32 -> option ty) (st : salState) (ws : weakState) : Prop := {
wcAddrs : forall addr, concAddr ctx st addr;
wcTmp1 : forall r, concReg st ws r
}.
End weakTy2.
Module Create (_Sys : WEAK_UPDATE_TYPE_SYSTEM) : STACK_READY_TYPE_SYSTEM
with Definition ty := _Sys.ty
with Definition mastate := condState weakState
with Definition mcontext := int32 -> option _Sys.ty
with Definition hasTy := _Sys.hasTy
with Definition mconc := condConc (weakConc _Sys.hasTy).
Module IntermediateTySys <: STACK_READY_TYPE_SYSTEM.
Import _Sys.
Module Mac := M.
Definition ty := ty.
Definition print_ty := print_ty.
Definition mastate := weakState.
Definition print_mastate ws :=
let (default, elems) := SalRegMap.elements ws in
print_weakState (fun f => iter f elems).
Definition mcontext := int32 -> option ty.
Definition mconc := weakConc hasTy.
Hint Unfold mconc.
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 salExpOpt_ok (x y : option salExp) := x = y \/ y = None.
Hint Unfold salExpOpt_ok.
Definition salExpOpt_ok_dec : forall (x y : option salExp), {salExpOpt_ok x y} + {~salExpOpt_ok x y}.
Definition salExpOpt_popt : forall (x y : option salExp), pred_option (salExpOpt_ok x y).
Definition subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
Definition hasTy := hasTy.
Definition tyTop := tyTop.
Definition tyTopSound := tyTopSound.
Hint Resolve tyTopSound.
Definition tyConst := tyConst.
Definition tyConstSound1 := tyConstSound1.
Definition tyConstSound2 := tyConstSound2.
Definition isTyConst := isTyConst.
Definition subTy := subTy.
Hint Unfold hasTy.
Hint Resolve tyConstSound1.
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}.
Lemma inHeap_apartFromCode : forall v,
inHeap v
-> apartFromCode v.
Hint Resolve inHeap_apartFromCode.
Lemma inHeap_not_too_high : forall v,
inHeap v
-> not_too_high v.
Hint Resolve inHeap_not_too_high.
Lemma inHeap_apartFromStack : forall v,
inHeap v
-> apartFromStack v.
Hint Resolve inHeap_apartFromStack.
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)).
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.
Theorem 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').
Hint Unfold mconc.
Hint Constructors weakConc.
Definition regFree : forall (r : salReg) (e : salExp),
pred_option (forall st v,
evalExp st e = evalExp (set_reg st r v) e).
Lemma get_mem32_flags : forall st fl a,
get_mem32
(Build_salState (SstRegs st) fl (SstMem st) (SstPc st)) a
= get_mem32 st a.
Lemma evalExp_flags : forall st fl e,
evalExp
(Build_salState (SstRegs st) fl (SstMem st) (SstPc st)) e
= evalExp st e.
Lemma concReg_easy : forall st r,
concReg st (SalRegMap.init None) r.
Hint Resolve concReg_easy.
Definition contains : forall (abs : mastate) (e : salExp),
sig_option (fun e' => forall ctx st,
mconc ctx st abs
-> evalExp st e = get_mem32 st (evalExp st e')).
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_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 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 IntermediateTySys.
Lemma bsub32_eq : forall n,
bsub32 n n = bzero32.
Ltac clear_one :=
match goal with
| [ H : _ |- _ ] => clear H
end.
Ltac clear_all := repeat clear_one.
Lemma mult_inc : forall k n,
k > 1
-> n > 1
-> k * n >= 2 * n.
Import Datatypes.
Lemma pow2_gt_1 : forall len, pow2 (S len) > 1.
Hint Resolve pow2_gt_1.
Lemma bsub32_eq' : forall n1 n2,
bsub32 n1 n2 = bzero32
-> n1 = n2.
Module WithTesting <: TYPE_SYSTEM_WITH_TESTING.
Module Sys := IntermediateTySys.
Import Sys.
Definition lowerTy t :=
match t with
| Const n => tyConst n
| Cust t' => t'
| _ => tyTop
end.
Hint Resolve tyTopSound.
Lemma lowerTy_sound : forall v ctx t,
stackHasTy _Sys.hasTy ctx v t
-> _Sys.hasTy (ctxCust ctx) v (lowerTy t).
Hint Resolve lowerTy_sound.
Definition raiseTy t :=
match _Sys.isTyConst t with
| SNone =>
if _Sys.subTy _Sys.tyTop t
then Top _
else Cust t
| SSome n _ => Const _ n
end.
Lemma raiseTy_sound : forall v ctx t,
_Sys.hasTy (ctxCust ctx) v t
-> stackHasTy _Sys.hasTy ctx v (raiseTy t).
Definition doCastEq : forall r n (abs : stateDescription (stackTy Sys.ty)
(stackState Sys.ty Sys.mastate)),
{abs' : stateDescription (stackTy Sys.ty) (stackState Sys.ty Sys.mastate)
| forall ctx st,
typeMconc (stackHasTy Sys.hasTy) (stackConc Sys.hasTy Sys.mconc) ctx st abs
-> get_reg st r = n
-> typeMconc (stackHasTy Sys.hasTy) (stackConc Sys.hasTy Sys.mconc) ctx st abs'}.
Definition doCastNeq : forall r n (abs : stateDescription (stackTy Sys.ty)
(stackState Sys.ty Sys.mastate)),
{abs' : stateDescription (stackTy Sys.ty) (stackState Sys.ty Sys.mastate)
| forall ctx st,
typeMconc (stackHasTy Sys.hasTy) (stackConc Sys.hasTy Sys.mconc) ctx st abs
-> get_reg st r <> n
-> typeMconc (stackHasTy Sys.hasTy) (stackConc Sys.hasTy Sys.mconc) ctx st abs'}.
Lemma bsub_comm : forall n1 n2,
bsub32 n1 n2 = bzero32
-> bsub32 n2 n1 = bzero32.
Hint Resolve bsub_comm.
Definition 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 WithTesting.
Module CondSys := AddCond(WithTesting).
Import CondSys.
Definition ty := ty.
Definition print_ty := print_ty.
Definition mastate := mastate.
Definition print_mastate := print_mastate.
Definition mcontext := mcontext.
Definition mconc := mconc.
Definition subMastate := subMastate.
Definition hasTy := hasTy.
Definition tyTop := tyTop.
Definition tyTopSound := tyTopSound.
Definition tyConst := tyConst.
Definition tyConstSound1 := tyConstSound1.
Definition tyConstSound2 := tyConstSound2.
Definition isTyConst := isTyConst.
Definition subTy := subTy.
Definition typeof := typeof.
Definition typeofLoad := typeofLoad.
Definition checkStore := checkStore.
Definition effectOfCmd := effectOfCmd.
Definition doStackWrite := doStackWrite.
Definition effectOfJump := effectOfJump.
Definition effectOfConditionalJump := effectOfConditionalJump.
Definition viewShiftOfJump := viewShiftOfJump.
End Create.
End Make.