| Even/odd abstract interpretation |
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.SimpleTypes.
Require Import ProofOS.AbsInt.SimpleDriver.
Set Implicit Arguments.
Inductive evenOddTy : Set :=
| Anything
| Constant : int32 -> evenOddTy
| Even
| Odd.
Parameter print_evenOddTy : evenOddTy -> unit.
Definition isEven (v : int32) :=
match v with
| Vcons false _ _ => True
| _ => False
end.
Definition isOdd (v : int32) :=
match v with
| Vcons true _ _ => True
| _ => False
end.
Definition to_int32 : forall size, vector bool size
-> size = 32 -> int32.
Definition parity_dec : forall (v : int32), {isEven v} + {isOdd v}.
Inductive hasEvenOddTy : int32 -> evenOddTy -> Prop :=
| HT_Anything : forall v,
hasEvenOddTy v Anything
| HT_Constant : forall v,
hasEvenOddTy v (Constant v)
| HT_Even : forall v,
isEven v
-> hasEvenOddTy v Even
| HT_Odd : forall v,
isOdd v
-> hasEvenOddTy v Odd.
Lemma rewrite_double : forall n,
n + (n + 0) = 2 * n.
Lemma merge_times : forall m1 m2 n,
n * m1 + n * m2 = n * (m1 + m2).
Import Datatypes.
Lemma merge_times_S : forall m1 m2 n,
n * m1 + S (n * m2) = S (n * (m1 + m2)).
Lemma merge_times_S2 : forall m1 m2 n,
S (n * m1) + n * m2 = S (n * (m1 + m2)).
Lemma merge_times_S3 : forall m1 m2,
S (2 * m1) + S (2 * m2) = 2 * (m1 + m2 + 1).
Hint Rewrite rewrite_double merge_times merge_times_S
merge_times_S2 merge_times_S3 : fixup.
Hint Rewrite mod2_bool_2 mod2_bool_S2 : fixup.
Ltac int32_arith :=
let v1 := fresh "v1" with v2 := fresh "v2"
with Hv1 := fresh "Hv1" with Hv2 := fresh "Hv2"
with Hv1Eq := fresh "Hv1Eq" with Hv2Eq := fresh "Hv2Eq" in
(intros v1 v2 Hv1 Hv2;
simpl; unfold int32, Bvector in *;
VSntac Hv1Eq v1; VSntac Hv2Eq v2;
rewrite Hv1Eq in Hv1; rewrite Hv2Eq in Hv2;
simpl in *;
destruct (Vhead v1); try tauto;
destruct (Vhead v2); try tauto;
autorewrite with fixup; trivial).
Lemma add_even_even : forall v1 v2,
isEven v1
-> isEven v2
-> isEven (eval_arith Add v1 v2).
Lemma add_even_odd : forall v1 v2,
isEven v1
-> isOdd v2
-> isOdd (eval_arith Add v1 v2).
Lemma add_odd_even : forall v1 v2,
isOdd v1
-> isEven v2
-> isOdd (eval_arith Add v1 v2).
Lemma add_odd_odd : forall v1 v2,
isOdd v1
-> isOdd v2
-> isEven (eval_arith Add v1 v2).
Hint Resolve add_even_even add_even_odd add_odd_even add_odd_odd.
Module EvenOddTySys <: SIMPLE_TYPE_SYSTEM.
Definition ty := evenOddTy.
Definition print_ty := print_evenOddTy.
Definition hasTy := hasEvenOddTy.
Hint Unfold hasTy.
Hint Constructors hasEvenOddTy.
Definition tyTop := Anything.
Theorem tyTopSound : forall v, hasTy v tyTop.
Definition tyConst := Constant.
Theorem tyConstSound1 : forall v, hasTy v (tyConst v).
Theorem tyConstSound2 : forall v1 v2, hasTy 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 v,
hasTy v t1 -> hasTy v t2).
Definition relaxTy : forall (t : ty), {t' : ty | forall v, hasTy v t -> hasTy v t'}.
Definition 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 EvenOddTySys.
Module Verifier (Param : DRIVER_REGIONS).
Module MyParam <: DRIVER_PARAM.
Module Regions := Param.
Module Sys := EvenOddTySys.
End MyParam.
Module Dr := Driver(MyParam).
End Verifier.