From 0cba965562a367a8eb8a4fcf493b2ee24e5df485 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 23 Oct 2019 07:49:07 +0200
Subject: [PATCH] [wp] removed semantics dir
---
src/plugins/wp/semantics/Cil.v | 49 -----
src/plugins/wp/semantics/Datatype.v | 290 ---------------------------
src/plugins/wp/semantics/Layout.v | 120 -----------
src/plugins/wp/semantics/Machine.v | 73 -------
src/plugins/wp/semantics/Makefile | 23 ---
src/plugins/wp/semantics/Pointer.v | 41 ----
src/plugins/wp/semantics/Primitive.v | 23 ---
src/plugins/wp/semantics/Semantics.v | 77 -------
src/plugins/wp/semantics/Typing.v | 78 -------
src/plugins/wp/semantics/Values.v | 109 ----------
src/plugins/wp/semantics/coqide.sh | 1 -
11 files changed, 884 deletions(-)
delete mode 100644 src/plugins/wp/semantics/Cil.v
delete mode 100644 src/plugins/wp/semantics/Datatype.v
delete mode 100644 src/plugins/wp/semantics/Layout.v
delete mode 100644 src/plugins/wp/semantics/Machine.v
delete mode 100644 src/plugins/wp/semantics/Makefile
delete mode 100644 src/plugins/wp/semantics/Pointer.v
delete mode 100644 src/plugins/wp/semantics/Primitive.v
delete mode 100644 src/plugins/wp/semantics/Semantics.v
delete mode 100644 src/plugins/wp/semantics/Typing.v
delete mode 100644 src/plugins/wp/semantics/Values.v
delete mode 100755 src/plugins/wp/semantics/coqide.sh
diff --git a/src/plugins/wp/semantics/Cil.v b/src/plugins/wp/semantics/Cil.v
deleted file mode 100644
index 285ecdf66d3..00000000000
--- a/src/plugins/wp/semantics/Cil.v
+++ /dev/null
@@ -1,49 +0,0 @@
-Require Import Datatype.
-Require Import Primitive.
-
-Parameter cvar : Data.
-Parameter cfield : Data.
-Parameter ctypedef : Data.
-Parameter label : Data.
-
-Inductive cref : Set :=
- | Rvoid : cref
- | Rint : cint -> cref
- | Rflt : cflt -> cref
- | Rdef : ctypedef -> cref.
-
-Inductive ctype : Set :=
- | Cptr : cref -> ctype
- | Cint : cint -> ctype
- | Cflt : cflt -> ctype
- | Carray : ctype -> Z -> ctype
- | Cstruct : [ cfield => ctype ] -> ctype
- | Cunion : [ cfield => ctype ] -> ctype.
-
-Record cenv : Type := {
- g_var : cvar -> ctype ;
- g_typedef : ctypedef -> ctype
-}.
-
-Inductive lval : Set :=
- | Lvar : cvar -> lval
- | Lshift : lval -> exp -> lval
- | Lfield : lval -> cfield -> lval
- | Lderef : exp -> lval
-
-with exp : Set :=
- | Lval : lval -> exp
- | AddrOf : lval -> exp
- | Shift : exp -> exp -> exp
- | Op : op -> exp -> exp -> exp.
-
-Inductive instr : Set :=
- | Instr : lval -> exp -> instr
- | Guard : exp -> instr.
-
-Definition stmt := ( label * instr * label )%type.
-Definition program := List.list stmt.
-
-
-
-
diff --git a/src/plugins/wp/semantics/Datatype.v b/src/plugins/wp/semantics/Datatype.v
deleted file mode 100644
index ccff6e67cec..00000000000
--- a/src/plugins/wp/semantics/Datatype.v
+++ /dev/null
@@ -1,290 +0,0 @@
-(** Basic Datatypes *)
-
-Set Implicit Arguments.
-
-Require Export Bool.
-Require Export Reals.
-Require Export ZArith.
-Require Export Program.
-Open Scope Z_scope.
-
-(** ** Tactics for finishing proof trees. *)
-
-Ltac forward :=
- repeat (first [ split | intros ]) ;
- try discriminate ;
- try contradiction ;
- try tauto ;
- try constructor ;
- try (apply False_ind ; omega ; fail) ;
- try (apply False_ind ; auto with zarith ; fail) ;
- auto with zarith.
-
-Ltac finish := forward ; fail.
-
-Tactic Notation "by" tactic(A) := A ; finish.
-
-(** ** Empty Set. *)
-
-Inductive Void : Set := .
-
-(** ** Unit Set. *)
-
-Inductive Unit : Set := unit.
-
-(** ** Decidability. *)
-
-Definition decide P := {P}+{~P}.
-
-Definition isTrue p := (p = true).
-Definition isFalse p := (p = false).
-(*
-Lemma not_is_true : forall p, ~(isTrue p) -> isFalse p.
-Lemma not_is_false : forall p, ~(isFalse p) -> isTrue p.
-*)
-
-Coercion bool2p := isTrue.
-
-Lemma split_andb : forall p q, p && q <-> p /\ q.
-Proof. intros p q. induction p ; induction q ; intuition. Qed.
-
-Lemma split_orb : forall p q, p || q <-> p \/ q.
-Proof. intros p q. induction p ; induction q ; intuition. Qed.
-
-(** ** Types with decidable equality. *)
-
-Record Data := {
- type :> Set ;
- eqdec : forall (a b : type), decide (a=b)
-}.
-
-Definition eqb {D : Data} (a b : D) :=
- match eqdec _ a b with
- | left _ => true
- | right _ => false
- end.
-
-Notation "a == b" := (@eqb _ a b) (at level 70).
-
-(** ** Tactics for proof by case on Data equality. *)
-
-Lemma eqb_true : forall (D : Data) (x y : D), x=y -> (x==y) = true.
-Proof. intros. rewrite H. unfold eqb. induction (eqdec _ y y). trivial. auto. Qed.
-
-Lemma eqb_false : forall (D : Data) (x y : D), x<>y -> (x==y) = false.
-Proof. intros. unfold eqb. induction (eqdec _ x y). rewrite a in H. intuition. trivial. Qed.
-
-Ltac equality a b :=
- let Eq := fresh "Eq_" a "_" b in
- let Neq := fresh "Neq_" a "_" b in
- induction (eqdec _ a b) as [ Eq | Neq ] ;
- [ try (rewrite Eq in *) ; try (rewrite eqb_true in *)
- | try (rewrite Neq in *) ; try (rewrite eqb_false in *)
- ] ; auto.
-
-(** ** Dependent Equalities. *)
-
-(** Lift an equality [x = y] into an equality over [u : B x] and [v : B y]. *)
-Definition lift_eq {A : Set} (B : A -> Set) {x y : A} (p : x = y) : B x -> B y -> Prop :=
- let P := fun z => B x -> B z -> Prop in
- let E := (@eq (B x)) in
- eq_rect x P E y p.
-
-(** List is the expected equality. *)
-Lemma lift_eq_is_eq :
- forall (A : Set) (B : A -> Set) x,
- lift_eq B (eq_refl x) = (fun (y z : B x) => y = z).
-Proof. intros. simpl. trivial. Qed.
-
-(** ** Typical Data *)
-
-Program Definition Int : Data := {| type := Z |}.
-Next Obligation. apply Z.eq_dec. Qed.
-
-Lemma fst_neq : forall A B, forall (p q : A*B), fst p <> fst q -> p <> q.
- Proof. intros. unfold not. intro E. rewrite E in H. auto. Qed.
-Lemma snd_neq : forall A B, forall (p q : A*B), snd p <> snd q -> p <> q.
- Proof. intros. unfold not. intro E. rewrite E in H. auto. Qed.
-
-Program Definition Pair (A B : Data) : Data := {| type := A * B |}.
-Next Obligation.
- elim (eqdec A t1 t) ; elim (eqdec B t2 t0) ; intros.
- * left. rewrite a,a0. trivial.
- * right. apply snd_neq. auto.
- * right. apply fst_neq. auto.
- * right. apply fst_neq. auto.
-Qed.
-
-(** ** Functional Updates *)
-
-Definition select {A B : Type} {P : A -> Prop} (s : forall a, decide(P a)) (a b : A -> B)
- := fun k => if s k then a k else b k.
-
-(** ** Finite Environments *)
-
-Inductive env {A B : Type} : Type :=
- | empty : env
- | add : A -> B -> env -> env.
-
-Notation "[ A => B ]" := (@env A B).
-
-Fixpoint map {A B C : Type} (f : A -> B -> C) (e : [A => B]) : [A => C] :=
- match e with
- | empty => empty
- | add x v e => add x (f x v) (map f e)
- end.
-
-Fixpoint find {A : Data} {B : Type} (x : A) e (d : B) :=
- match e with
- | empty => d
- | add x' v e => if x == x' then v else find x e d
- end.
-
-Fixpoint bind {A : Data} {B : Type} (x : A) (v : B) e : Prop :=
- match e with
- | empty => False
- | add x' v' e => if x == x' then v = v' else bind x v e
- end.
-
-Lemma bind_map_exists :
- forall (A : Data) (B C : Type) (f : A -> B -> C),
- forall x w e, bind x w (map f e) -> exists v, bind x v e /\ w = f x v.
-Proof.
- intros.
- induction e.
- * by (simpl in H).
- * simpl in H. equality x a.
- - exists b. simpl. rewrite eqb_true ; auto.
- - simpl. rewrite eqb_false ; auto.
-Qed.
-
-Lemma bind_map :
- forall (A : Data) (B C : Type) (f : A -> B -> C),
- forall x v e, bind x v e -> bind x (f x v) (map f e).
-Proof.
- intros.
- induction e ; simpl in * ; auto.
- equality x a ; rewrite H ; auto.
-Qed.
-
-Inductive subset {A B : Type} : [ A => B ] -> [ A => B ] -> Prop :=
- | Sub_empty : subset empty empty
- | Sub_skip : forall a b w1 w2, subset w1 w2 -> subset w1 (add a b w2)
- | Sub_same : forall a b w1 w2, subset w1 w2 -> subset (add a b w1) (add a b w2).
-
-(** ** Records (dependent maps) *)
-
-Inductive record {A : Type} : [ A => Type ] -> Type :=
- | Rempty : record empty
- | Rfield : forall (a:A) {t:Type} (v:t)
- {r:[A => Type]} (R:record r),
- record (add a t r).
-
-Notation "{[ m ]}" := (record m).
-
-Inductive union {A : Type} : [ A => Type ] -> Type :=
- | Uempty : union empty
- | Uskip : forall (a:A) { t: Type } (* no value *)
- { u: [A => Type] } (U:union u),
- union (add a t u)
- | Ufield : forall (a:A) { t: Type } (v:t) (* some value *)
- { u: [A => Type] } (U:union u),
- union (add a t u).
-
-Notation "{[ m ?]}" := (union m).
-
-(** ** Positive integers *)
-
-Coercion Z.pos : positive >-> Z.
-
-(** ** Finite integers *)
-
-Record range (n : Z) : Type :=
- { index :> Z ; in_range : 0 <= index < n }.
-
-Definition range_dec (n k : Z) : decide (0 <= k < n).
-Proof.
- induction (Z_le_dec 0 k) ; induction (Z_lt_dec k n) ; try (by left) ; try (by right).
-Qed.
-
-Fixpoint iter (P : nat -> bool) n :=
- match n with
- | O => true
- | S n => P n && iter P n
- end.
-
-Lemma iter_forall :
- forall P n, iter P n -> (forall k, (k < n)%nat -> P k).
-Proof.
- intros P n.
- induction n.
- * simpl. intros. omega.
- * simpl. intros Step k Rk.
- rewrite split_andb in Step.
- assert (Rn : (k <= n)%nat) by omega.
- induction (le_lt_eq_dec k n) as [Lt | Eq] ; auto with arith.
- + by (apply IHn).
- + by (rewrite Eq).
-Qed.
-
-(** ** Arrays of known size *)
-
-Definition array (A : Type) (n : Z) : Type := range n -> A.
-Notation "a [ n ]" := (array a n) (at level 10).
-
-Definition slice {A} p n (w : Z -> A) : A[n] := fun k : range n => w (p+k).
-
-Definition get {A n} (a : A[n]) k rk := a {| index := k ; in_range := rk |}.
-Implicit Arguments get [A n].
-
-Definition split {n m} (k : range (n+m)) : {0 <= k < n}+{0<= k-n < m}.
-Proof.
- generalize (in_range k). intro Rk.
- induction (range_dec n k) ; [ left | right] ; forward.
-Qed.
-
-Definition concat {A n m} (a : A[n]) (b : A[m]) : A[n+m] :=
- fun k : range (n+m) =>
- match split k with
- | left p => get a k p
- | right q => get b (k-n) q
- end.
-
-Lemma concat_l {A n m} (a : A[n]) (b : A[m]) :
- forall (k : range (n+m)) (r : 0 <= k < n), (concat a b) k = get a k r.
-Proof.
- intros.
- unfold concat.
- destruct (split k).
- + apply f_equal. apply proof_irrelevance.
- + generalize (in_range k). intros. omega.
-Qed.
-
-Lemma concat_r {A n m} (a : A[n]) (b : A[m]) :
- forall (k : range (n+m)) (r : 0 <= k-n < m), (concat a b) k = get b (k-n) r.
-Proof.
- intros.
- unfold concat.
- destruct (split k).
- + generalize (in_range k). intros. omega.
- + apply f_equal. apply proof_irrelevance.
-Qed.
-
-Lemma array_inj {A n} : forall (a b : A[n]),
- (forall k : range n, a k = b k) -> a = b.
-Proof.
- intros a b Elt.
- extensionality k.
- apply Elt.
-Qed.
-
-Record vector (A : Type) : Type := { size ; elt :> A[size] }.
-Notation "a []" := (vector a) (at level 10).
-
-Definition compatible {A n m} (a : A[n]) (b : A[m]) :=
- forall k (ka : 0 <= k < n) (kb : 0 <= k < m),
- get a k ka = get b k kb.
-
-
-
-
diff --git a/src/plugins/wp/semantics/Layout.v b/src/plugins/wp/semantics/Layout.v
deleted file mode 100644
index 6ecdffc4f5e..00000000000
--- a/src/plugins/wp/semantics/Layout.v
+++ /dev/null
@@ -1,120 +0,0 @@
-Require Import Datatype.
-Require Import Pointer.
-Require Import Machine.
-
-Open Scope Z_scope.
-
-Program Definition empty_layout (A : Type) : layout A := {|
- sizeof := 0 ;
- encoding := fun p w => True
-|}.
-Next Obligation. intuition. Qed.
-
-Program Definition interpret {A B} (phi : B -> A) : layout A -> layout B :=
- fun enc => {| encoding := fun v w => enc (phi v) w ; sizeof := sizeof enc |}.
-Next Obligation.
- by (apply (positive enc)).
-Qed.
-Next Obligation.
- apply (footprint enc H).
-Qed.
-
-Program Definition concat {A B} : layout A -> layout B -> layout (A*B) :=
- fun a b => {|
- sizeof := sizeof a + sizeof b ;
- encoding := fun p w => (a (fst p) w /\ b (snd p) (w <+> sizeof a))
- |}.
-Next Obligation.
- generalize (positive a).
- generalize (positive b).
- auto with zarith.
-Qed.
-Next Obligation.
- simpl.
- cut (b b0 (wa <+> sizeof a) <-> b b0 (wb <+> sizeof a)).
- cut (a a0 wa <-> a a0 wb).
- intuition.
- * apply (footprint a).
- unfold eq_range.
- intros k R. apply H.
- generalize (positive a).
- generalize (positive b).
- auto with zarith.
- * apply (footprint b).
- unfold eq_range.
- intros k R. unfold offset. apply H.
- generalize (positive a).
- generalize (positive b).
- auto with zarith.
-Defined.
-
-Program Definition superpose {A B} : layout A -> layout B -> layout (A * B) :=
- fun a b => {|
- sizeof := Z.max (sizeof a) (sizeof b) ;
- encoding := fun p w => (a (fst p) w /\ b (snd p) w)
- |}.
-Next Obligation.
- apply Z.max_case. apply (positive a). apply (positive b).
-Qed.
-Next Obligation.
- simpl.
- cut (b b0 wa <-> b b0 wb).
- cut (a a0 wa <-> a a0 wb).
- intuition.
- * apply (footprint a).
- unfold eq_range.
- intros k R. apply H.
- generalize (Z.le_max_l (sizeof a) (sizeof b)).
- omega.
- * apply (footprint b).
- unfold eq_range.
- intros k R. apply H.
- generalize (Z.le_max_r (sizeof a) (sizeof b)).
- omega.
-Defined.
-
-Program Definition concat_n {A} : layout A -> forall n, layout (A[n]) :=
- fun a n => {|
- sizeof := Z.max 0 (n * sizeof a) ;
- encoding := fun v w => forall (k : range n), a (v k) (w <+> k * sizeof a)
- |}.
-Next Obligation.
- by (apply Z.le_max_l).
-Qed.
-Next Obligation.
- cut (forall k : range n, a (v k) (wa <+> k * sizeof a)
- <-> a (v k) (wb <+> k * sizeof a)).
- intuition ; apply H0 ; apply H1.
- intro k.
- apply (footprint a).
- unfold eq_range, forall_range, offset. intros i Ri. simpl. apply H.
- generalize (in_range k). intro Rk.
- generalize (positive a). intro Pa.
- rewrite Z.max_r ; auto with zarith.
- assert (R1 : k <= n-1) by auto with zarith.
- assert (R2 : k * sizeof a <= (n-1) * sizeof a)
- by (apply Zmult_le_compat_r ; forward).
- assert (R3 : (n-1) * sizeof a = n * sizeof a - sizeof a) by ring.
- rewrite R3 in R2.
- auto with zarith.
-Defined.
-
-Program Definition option_layout {A} : layout A -> layout (option A) :=
- fun a => {|
- sizeof := sizeof a ;
- encoding := fun v w =>
- match v with
- | None => forall x, not (a x w)
- | Some x => a x w
- end
- |}.
-Next Obligation. exact (positive a). Qed.
-Next Obligation.
- induction v.
- + apply (footprint a H).
- + generalize (footprint a H).
- intuition.
- apply (H1 x). by (rewrite H0).
- apply (H1 x). by (rewrite <- H0).
-Qed.
-
diff --git a/src/plugins/wp/semantics/Machine.v b/src/plugins/wp/semantics/Machine.v
deleted file mode 100644
index a240a231d19..00000000000
--- a/src/plugins/wp/semantics/Machine.v
+++ /dev/null
@@ -1,73 +0,0 @@
-Require Import Datatype.
-Require Import Primitive.
-Require Import Pointer.
-
-Set Implicit Arguments.
-
-Inductive byte : Type :=
- | Byte : forall b, 0 <= b < 255 -> byte
- | Ptr : Addr -> nat -> byte
- | Undef : byte.
-
-Inductive perm := Read | Write.
-Definition grants p q := p = Write \/ q = Read.
-Definition granted q p := p = Write \/ q = Read.
-
-Definition bytes := Z -> byte.
-Definition perms := Z -> perm.
-
-Record layout (A : Type) := {
- encoding :> A -> bytes -> Prop ;
- sizeof : Z ;
- positive : 0 <= sizeof ;
- footprint : forall {wa wb},
- wa =/ sizeof wb ->
- forall v, encoding v wa <-> encoding v wb
-}.
-
-Record architecture := {
- int_layout : cint -> layout Z ;
- flt_layout : cflt -> layout R ;
- ptr_layout : layout Addr ;
- char_size : sizeof (int_layout char) = 1
-}.
-
-Record mem := {
- byte_at : Addr -> byte ;
- perm_at : Addr -> perm ;
- arch :> architecture
-}.
-
-Definition undef {A} : A -> byte := fun _ => Undef.
-
-Definition mload (m : mem) (p : Addr) (n : Z) : bytes :=
- select (range_dec n) (byte_at m @ p) undef.
-
-Definition store (m : mem) (p : Addr) n (v : bytes) : mem :=
-{|
- arch := m ;
- perm_at := perm_at m ;
- byte_at := select (ptr_range p n) (v & p) (byte_at m)
-|}.
-
-Definition valid (pi : perm) (m : mem) (p : Addr) n : Prop :=
- (fun k => grants (perm_at m (shift p k)) pi) /: n.
-
-Record read {A} (T : layout A)
- (m : mem) (p : Addr) (a : A) : Prop
-:= {
- valid_read :> valid Read m p (sizeof T) ;
- value_read :> T a (mload m p (sizeof T))
-}.
-
-Record written {A} (T : layout A)
- (m : mem) (p : Addr) (a : A) (v : bytes) (m' : mem) : Prop
-:= {
- valid_write :> valid Write m p (sizeof T) ;
- value_write :> T a v ;
- mem_write : m' = store m p (sizeof T) v
-}.
-
-Definition write {A} (T : layout A)
- (m : mem) (p : Addr) (a : A) (m' : mem) : Prop
- := exists v, written T m p a v m'.
diff --git a/src/plugins/wp/semantics/Makefile b/src/plugins/wp/semantics/Makefile
deleted file mode 100644
index 32ad89fce19..00000000000
--- a/src/plugins/wp/semantics/Makefile
+++ /dev/null
@@ -1,23 +0,0 @@
-
-.PHONY: all depend
-
-MODULES= Datatype Primitive Cil Pointer Machine Layout Values Typing Semantics
-
-INCLUDES= -I .
-SOURCES=$(addsuffix .v, $(MODULES))
-OBJECTS=$(addsuffix .vo, $(MODULES))
-
-all: $(OBJECTS)
-
-.SUFFIXES: .v .vo
-
-.v.vo:
- coqc $(INCLUDES) $<
-
-depend:
- coqdep $(INCLUDES) $(SOURCES) > .depend
-
-clean:
- rm -f *~ *.vo *.glob
-
-sinclude .depend
diff --git a/src/plugins/wp/semantics/Pointer.v b/src/plugins/wp/semantics/Pointer.v
deleted file mode 100644
index 8d9ed33f991..00000000000
--- a/src/plugins/wp/semantics/Pointer.v
+++ /dev/null
@@ -1,41 +0,0 @@
-Require Import Datatype.
-Open Scope Z_scope.
-
-Parameter base : Data.
-
-Definition Addr := Pair base Int.
-
-Definition shift (p : Addr) (k : Z) : Addr := ( fst p , snd p + k ).
-
-Definition separated p n q m :=
- forall i j, 0 <= i <= n -> 0 <= j <= m -> shift p i <> shift q j.
-
-Definition in_ptr_range (p : Addr) n q :=
- fst p = fst q /\ snd p <= snd q < snd p + n.
-
-Definition ptr_range (p:Addr) n q : decide ( in_ptr_range p n q ).
-Proof.
- unfold in_ptr_range.
- induction (eqdec base (fst p) (fst q)) as [Eq | Neq] ;
- induction (range_dec n (snd q - snd p)) ;
- try (by left) ;
- try (by right).
-Qed.
-
-Definition read_at_ptr {A} (phi : Addr -> A) (p : Addr) : Z -> A
- := fun k => phi (shift p k).
-Infix "@" := read_at_ptr (at level 70).
-
-Definition copy_to_ptr {A} (phi : Z -> A) (p : Addr) : Addr -> A
- := fun (q : Addr) => phi (snd q - snd p).
-Infix "&" := copy_to_ptr (at level 70).
-
-Definition offset {A:Type} (m : Z -> A) (p:Z) := fun k => m (p+k).
-Infix "<+>" := offset (at level 70).
-
-Definition forall_range (phi : Z -> Prop) n : Prop := forall k, 0 <= k < n -> phi k.
-Infix "/:" := forall_range (at level 70).
-
-Definition eq_range {A : Type} n (a b : Z -> A) := (fun k => a k = b k) /: n.
-Notation "a =/ n b" := (eq_range n a b) (at level 70, n at level 0).
-
diff --git a/src/plugins/wp/semantics/Primitive.v b/src/plugins/wp/semantics/Primitive.v
deleted file mode 100644
index be075db364a..00000000000
--- a/src/plugins/wp/semantics/Primitive.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Require Import Datatype.
-
-Parameter cint : Data.
-Parameter cflt : Data.
-Parameter char : cint.
-
-Parameter irange : cint -> Z -> Prop.
-Parameter frange : cflt -> R -> Prop.
-
-Definition ptype := (cint + cflt)%type.
-Definition prim := (Z + R)%type.
-
-Inductive prange : ptype -> prim -> Prop :=
- | PRIM_int : forall i x, irange i x -> prange (inl i) (inl x)
- | PRIM_flt : forall f u, frange f u -> prange (inr f) (inr u).
-
-Parameter op : Data.
-Parameter typeof_op : op -> ptype -> ptype -> ptype -> Prop.
-Parameter sem_op : op -> prim -> prim -> prim -> Prop.
-
-Inductive prim_domain : prim -> forall {t : Type}, t -> Prop :=
- | DOMAIN_int : forall x, prim_domain (inl x) x
- | DOMAIN_flt : forall u, prim_domain (inr u) u.
diff --git a/src/plugins/wp/semantics/Semantics.v b/src/plugins/wp/semantics/Semantics.v
deleted file mode 100644
index 7afa98620b4..00000000000
--- a/src/plugins/wp/semantics/Semantics.v
+++ /dev/null
@@ -1,77 +0,0 @@
-Require Import Datatype.
-Require Import Primitive.
-Require Import Cil.
-Require Import Pointer.
-Require Import Machine.
-Require Import Values.
-Require Import Typing.
-
-Record Compiler := { cc_env :> Gamma ; cc_link : cvar -> base }.
-
-Inductive sem_lval (G : Compiler) (m : mem) : lval -> Addr -> Prop :=
-
- | Svar : forall x,
- (* ----------------------------------------------- *)
- sem_lval G m (Lvar x) ( G.(cc_link) x , 0 )
-
- | Sshift_l : forall l t {d} (enc : layout d) p a (k:Z),
- typeof_lval G l t ->
- overlay m t enc ->
- sem_lval G m l p ->
- sem_exp G m a k ->
- (* ----------------------------------------------- *)
- sem_lval G m (Lshift l a) (shift p (sizeof enc * k))
-
- | Sfield_s : forall l s p f k,
- typeof_lval G l (Cstruct s) ->
- field_offset m f k s ->
- sem_lval G m l p ->
- (* ----------------------------------------------- *)
- sem_lval G m (Lfield l f) (shift p k)
-
- | Sfield_u : forall l s p f,
- typeof_lval G l (Cunion s) ->
- sem_lval G m l p ->
- (* ----------------------------------------------- *)
- sem_lval G m (Lfield l f) p
-
-with sem_exp (G : Compiler) (m : mem) : exp -> forall {T : Type}, T -> Prop :=
-
- | Sem_lval : forall l t p d (enc : layout d) (v : d),
- typeof_lval G l t ->
- overlay m t enc ->
- sem_lval G m l p ->
- read enc m p v ->
- (* ----------------------------------------------- *)
- sem_exp G m (Lval l) v
-
- | Sem_addrof : forall l p,
- sem_lval G m l p ->
- (* ----------------------------------------------- *)
- sem_exp G m (AddrOf l) p
-
- | Sem_shift : forall a p r {d} (enc : layout d) b k,
- typeof_exp G a (Cptr r) ->
- overlay m (typeof_ref G r) enc ->
- sem_exp G m a p ->
- sem_exp G m b k ->
- (* ----------------------------------------------- *)
- sem_exp G m (Shift a b) (shift p (sizeof enc * k))
-
- | Sem_op : forall op a b (ta tb tc : Type)
- pa (va : ta) pb (vb : tb) pc (vc : tc),
- prim_domain pa va -> sem_exp G m a va ->
- prim_domain pb vb -> sem_exp G m b vb ->
- prim_domain pc vc -> sem_op op pa pb pc ->
- (* ----------------------------------------------- *)
- sem_exp G m (Op op a b) vc
-
-.
-
-Theorem sem_welltyped (G : Compiler) (m : mem) :
- forall e t d (v : d),
- typeof_exp G e t ->
- sem_exp G m e v ->
- domain t d.
-Admitted.
-
diff --git a/src/plugins/wp/semantics/Typing.v b/src/plugins/wp/semantics/Typing.v
deleted file mode 100644
index 03b960f722a..00000000000
--- a/src/plugins/wp/semantics/Typing.v
+++ /dev/null
@@ -1,78 +0,0 @@
-Require Import Datatype.
-Require Import Primitive.
-Require Import Cil.
-
-Record Gamma : Type := {
- g_var : cvar -> ctype ;
- g_type : ctypedef -> ctype
-}.
-
-Definition typeof_ref (G : Gamma) (r : cref) : ctype :=
- match r with
- | Rvoid => Cint char
- | Rint i => Cint i
- | Rflt f => Cflt f
- | Rdef d => G.(g_type) d
- end.
-
-Definition ptype (p : ptype) : ctype :=
- match p with
- | inl i => Cint i
- | inr f => Cflt f
- end.
-
-Inductive typeof_exp (G : Gamma) : exp -> ctype -> Prop :=
-
- | Tlval : forall l t,
- typeof_lval G l t ->
- (* -------------------------------------- *)
- typeof_exp G (Lval l) t
-
- | Taddrof : forall l r,
- typeof_lval G l (typeof_ref G r) ->
- (* -------------------------------------- *)
- typeof_exp G (AddrOf l) (Cptr r)
-
- | Tshift : forall p k r i,
- typeof_exp G p (Cptr r) ->
- typeof_exp G k (Cint i) ->
- (* -------------------------------------- *)
- typeof_exp G (Shift p k) (Cptr r)
-
- | Top : forall op a pa b pb pr,
- typeof_op op pa pb pr ->
- typeof_exp G a (ptype pa) ->
- typeof_exp G b (ptype pb) ->
- (* --------------------------------------- *)
- typeof_exp G (Op op a b) (ptype pr)
-
-with typeof_lval (G : Gamma) : lval -> ctype -> Prop :=
-
- | Tvar : forall x,
- (* -------------------------------------- *)
- typeof_lval G (Lvar x) (G.(g_var) x)
-
- | Tshift_l : forall l t n e i,
- typeof_lval G l (Carray t n) ->
- typeof_exp G e (Cint i) ->
- (* -------------------------------------- *)
- typeof_lval G (Lshift l e) t
-
- | Tfield_s : forall l s f t,
- typeof_lval G l (Cstruct s) ->
- bind f t s ->
- (* -------------------------------------- *)
- typeof_lval G (Lfield l f) t
-
- | Tfield_u : forall l s f t,
- typeof_lval G l (Cunion s) ->
- bind f t s ->
- (* -------------------------------------- *)
- typeof_lval G (Lfield l f) t
-
- | Tderef : forall p r,
- typeof_exp G p (Cptr r) ->
- (* -------------------------------------- *)
- typeof_lval G (Lderef p) (typeof_ref G r)
-.
-
diff --git a/src/plugins/wp/semantics/Values.v b/src/plugins/wp/semantics/Values.v
deleted file mode 100644
index c85d2eb7073..00000000000
--- a/src/plugins/wp/semantics/Values.v
+++ /dev/null
@@ -1,109 +0,0 @@
-Require Import Datatype.
-Require Import Cil.
-Require Import Pointer.
-Require Import Machine.
-Require Import Layout.
-
-(** * Type Interpretation *)
-
-Definition Ccomp := [ cfield => ctype ].
-Definition Dcomp := [ cfield => Type ].
-
-Inductive domain : ctype -> Type -> Prop :=
- | Dptr : forall p, domain (Cptr p) Addr
- | Dint : forall i, domain (Cint i) Z
- | Dflt : forall f, domain (Cflt f) R
- | Darr : forall t n d, domain t d -> domain (Carray t n) (d[n])
- | Dstruct : forall s r, compound s r -> domain (Cstruct s) {[ r ]}
- | Dunion : forall s r, compound s r -> domain (Cunion s) {[ r ?]}
-
-with compound : Ccomp -> Dcomp -> Prop :=
- | Dempty : compound empty empty
- | Dfield : forall f t d T D,
- domain t d ->
- compound T D ->
- compound (add f t T) (add f d D).
-
-(** * Type Layout *)
-
-Definition head_record (f : cfield) T R (r : record (add f T R)) : T * record R :=
- match r with
- | Rempty => False
- | Rfield _ _ v _ r => (v,r)
- end.
-
-Definition struct_field (f : cfield) {T R} :
- layout T -> layout (record R) -> layout (record (add f T R))
- := fun a r => interpret (head_record f T R) (concat a r).
-
-Definition head_union (f : cfield) T U (u : union (add f T U)) : (option T) * union U :=
- match u with
- | Uempty => False
- | Uskip _ _ _ u => (None,u)
- | Ufield _ _ v _ u => (Some v,u)
- end.
-
-Definition union_field (f : cfield) {T R} :
- layout T -> layout (union R) -> layout (union (add f T R))
- := fun a r => interpret (head_union f T R) (superpose (option_layout a) r).
-
-Inductive overlay arch : ctype -> forall {t}, layout t -> Prop :=
- | Lptr : forall p, overlay arch (Cptr p) (ptr_layout arch)
- | Lint : forall i, overlay arch (Cint i) (int_layout arch i)
- | Lflt : forall f, overlay arch (Cflt f) (flt_layout arch f)
- | Lstruct : forall s r (e : layout {[ r ]}), struct_overlay arch s e -> overlay arch (Cstruct s) e
- | Lunion : forall s r (e : layout {[ r ?]}), union_overlay arch s e -> overlay arch (Cunion s) e
-
-with struct_overlay arch : Ccomp -> forall {r:Dcomp}, layout {[ r ]} -> Prop :=
- | Sempty : struct_overlay arch empty (empty_layout {[ empty ]})
- | Sfield : forall (f : cfield) t {d} (e : layout d)
- T {D} (R : layout {[ D ]}),
- overlay arch t e ->
- struct_overlay arch T R ->
- struct_overlay arch (add f t T) (struct_field f e R)
-
-with union_overlay arch : Ccomp -> forall {r:Dcomp}, layout {[ r ?]} -> Prop :=
- | Uempty : union_overlay arch empty (empty_layout {[ empty ?]})
- | Ufield : forall (f : cfield) t {d} (e : layout d)
- T {D} (R : layout {[ D ?]}),
- overlay arch t e ->
- union_overlay arch T R ->
- union_overlay arch (add f t T) (union_field f e R).
-
-Inductive field_offset arch : cfield -> Z -> Ccomp -> Prop :=
- | Ofs_field : forall f t T, field_offset arch f 0 (add f t T)
- | Ofs_next : forall f k g (t : ctype) {d} (enc : layout d) T,
- overlay arch t enc ->
- field_offset arch f k T ->
- field_offset arch f (sizeof enc + k) (add g t T).
-
-(** * Type and Domain Consistency *)
-
-Theorem overlay_domain : forall arch t d (e : layout d), overlay arch t e -> domain t d
- with struct_overlay_domain : forall arch T D (R : layout {[ D ]}), struct_overlay arch T R -> compound T D
- with union_overlay_domain : forall arch T D (R : layout {[ D ?]}), union_overlay arch T R -> compound T D.
-Proof.
-* intros.
- induction H.
- + apply Dptr.
- + apply Dint.
- + apply Dflt.
- + apply Dstruct.
- apply (struct_overlay_domain arch s r e). assumption.
- + apply Dunion.
- apply (union_overlay_domain arch s r e). assumption.
-* intros.
- induction H.
- - apply Dempty.
- - apply Dfield.
- + by (apply (overlay_domain arch t d e)).
- + by (apply (struct_overlay_domain arch T D R)).
-* intros.
- induction H.
- - apply Dempty.
- - apply Dfield.
- + by (apply (overlay_domain arch t d e)).
- + by (apply (union_overlay_domain arch T D R)).
-Qed.
-
-
diff --git a/src/plugins/wp/semantics/coqide.sh b/src/plugins/wp/semantics/coqide.sh
deleted file mode 100755
index 4e20bf4b06f..00000000000
--- a/src/plugins/wp/semantics/coqide.sh
+++ /dev/null
@@ -1 +0,0 @@
-coqide -I . $*
--
GitLab