| Integer pointer type-checking |
Require Import Bool Bvector Eqdep.
Require Import Asm.Util.Specif.
Require Import Asm.Util.Vector.
Require Import Asm.Util.Mod.
Require Import Asm.Util.Monad.
Require Import Asm.Util.Tactics.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.AbsInt.WeakUpdateTypes.
Require Import ProofOS.AbsInt.WeakDriver.
Require Import ProofOS.AbsInt.Sal.
Set Implicit Arguments.
Inductive intPtrTy : Set :=
| Anything
| Constant : int32 -> intPtrTy
| Ptr
| NnPtr.
Parameter print_intPtrTy : intPtrTy -> unit.
Inductive hasIntPtrTy : (int32 -> option intPtrTy) -> int32 -> intPtrTy -> Prop :=
| HT_Anything : forall ctx v,
hasIntPtrTy ctx v Anything
| HT_Constant : forall ctx v,
hasIntPtrTy ctx v (Constant v)
| HT_Ptr_Null : forall ctx,
hasIntPtrTy ctx bzero32 Ptr
| HT_Ptr_NonNull : forall ctx v,
ctx v = Some Anything
-> hasIntPtrTy ctx v Ptr
| HT_NnPtr : forall ctx v,
ctx v = Some Anything
-> hasIntPtrTy ctx v NnPtr.
Module IntPtrTySys <: WEAK_UPDATE_TYPE_SYSTEM.
Definition ty := intPtrTy.
Definition print_ty := print_intPtrTy.
Definition hasTy := hasIntPtrTy.
Hint Unfold hasTy.
Hint Constructors hasIntPtrTy.
Definition tyTop := Anything.
Definition tyTopSound := HT_Anything.
Definition tyConst := Constant.
Definition tyConstSound1 := HT_Constant.
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 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}.
Definition typeofCell : forall (t : ty),
sig_option (fun t' =>
forall ctx v,
hasTy ctx v t
-> ctx v = Some t').
Definition considerNeq : forall (t : ty) (v : int32),
{t' : ty
| forall ctx v1,
hasTy ctx v1 t
-> v1 <> v
-> hasTy ctx v1 t'}.
Definition 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'}.
Definition 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 IntPtrTySys.
Module Verifier (Param : DRIVER_REGIONS).
Module MyParam <: DRIVER_PARAM.
Module Regions := Param.
Module Sys := IntPtrTySys.
End MyParam.
Module Dr := Driver(MyParam).
End Verifier.