| A mock-up type system with only a Top type |
Require Import List TheoryList.
Require Import Asm.Util.Specif.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.AbsInt.Bounded.
Require Import ProofOS.AbsInt.Sal.
Require Import ProofOS.AbsInt.TypeSystem.
Require Import ProofOS.AbsInt.StackTypes.
Set Implicit Arguments.
Parameter print_int32_option : option int32 -> unit.
Parameter print_nostate : unit -> unit.
Module Make (Param : M86_PARAM_FIXED_CODE_AND_STACK).
Module Stack := StackTypes.Make(Param).
Import Stack.
Import TySys.
Import Fixed.
Import MySal.
Module MyTypeSystem <: STACK_READY_TYPE_SYSTEM.
Module Mac := M.
Definition ty := option int32.
Definition print_ty := print_int32_option.
Definition mastate := unit.
Definition print_mastate := print_nostate.
Definition mcontext := unit.
Definition mconc (ctx : mcontext) (st : Mac.mstate) (abs : mastate) := True.
Definition hasTy (ctx : mcontext) (v : int32) (t : ty) :=
match t with
| None => True
| Some n => v = n
end.
Definition tyTop : ty := None.
Hint Unfold hasTy.
Lemma tyTopSound' : forall ctx v, hasTy ctx v None.
Hint Resolve tyTopSound'.
Theorem tyTopSound : forall ctx v, hasTy ctx v tyTop.
Definition tyConst (n : int32) := Some 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).
Definition subTy : forall (t1 t2 : ty),
pred_option (forall ctx v,
hasTy ctx v t1 -> hasTy ctx v t2).
Definition subMastate : forall (abs1 abs2 : mastate),
pred_option (forall ctx st,
mconc ctx st abs1 -> mconc ctx st abs2).
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 MyTypeSystem.
End Make.