| Simple type system construction |
Require Import Arith List TheoryList.
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.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 of a simple type system |
Module Type SIMPLE_TYPE_SYSTEM.
Parameter ty : Set.
Parameter print_ty : ty -> unit.
Parameter hasTy : int32 -> ty -> Prop.
Parameter tyTop : ty.
Axiom tyTopSound : forall v, hasTy v tyTop.
Parameter tyConst : int32 -> ty.
Axiom tyConstSound1 : forall v, hasTy v (tyConst v).
Axiom tyConstSound2 : forall v1 v2, hasTy 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 v,
hasTy v t1 -> hasTy v t2).
Parameter typeofArith : forall (aop : arith_op) (t1 t2 : ty),
{t : ty
| forall v1 v2,
hasTy v1 t1
-> hasTy v2 t2
-> hasTy (eval_arith aop v1 v2) t}.
End SIMPLE_TYPE_SYSTEM.
Module Make (Param : M86_PARAM_FIXED_CODE_AND_STACK).
Module Stack := StackTypes.Make(Param).
Import Stack.
Import TySys.
Import Fixed.
Import MySal.
Definition dummyConc (_ : unit) (_ : M.mstate) (_ : unit) := True.
Section dummies.
Variable ty : Set.
Variable hasTy : int32 -> ty -> Prop.
Definition dummyHasTy (_ : unit) := hasTy.
End dummies.
Module Create (Sys : SIMPLE_TYPE_SYSTEM) : STACK_READY_TYPE_SYSTEM
with Definition ty := Sys.ty
with Definition mastate := unit
with Definition mcontext := unit
with Definition hasTy := dummyHasTy Sys.hasTy
with Definition mconc := dummyConc.
Import Sys.
Module Mac := M.
Definition ty := ty.
Definition print_ty := print_ty.
Definition mastate := unit.
Definition print_mastate (u : unit) := tt.
Definition mcontext := unit.
Definition mconc := dummyConc.
Definition subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
Definition hasTy := dummyHasTy hasTy.
Hint Unfold hasTy.
Definition tyTop := tyTop.
Lemma tyTopSound : forall ctx v, hasTy ctx v tyTop.
Hint Resolve tyTopSound.
Definition tyConst := 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 := isTyConst.
Definition subTy : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
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}.
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 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').
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').
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 Create.
End Make.