Make the string-ident maps available from Coq code

Makefile

@@ -58,7 +58,8 @@ FLOCQ=\
 VLIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
   Iteration.v Integers.v Archi.v Fappli_IEEE_extra.v Floats.v \
   Parmov.v UnionFind.v Wfsimpl.v \
-  Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v
+  Postorder.v FSetAVLplus.v IntvSets.v Decidableplus.v BoolEqual.v \
+  Symbols.v
 
 # Parts common to the front-ends and the back-end (in common/)
 

Makefile.extr

@@ -50,6 +50,7 @@ INCLUDES=$(patsubst %,-I %, $(DIRS))
 # Control of warnings:
 
 WARNINGS=-w +a-4-9-27 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
+extraction/%.cmi: WARNINGS +=-w -20-27-32..34-39-41-44..45
 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45
 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45
 cparser/pre_parser.cmx: WARNINGS += -w -41

arm/AsmToJSON.ml

@@ -37,7 +37,7 @@ let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; "
 
 type instruction_arg =
   | ALabel of positive
-  | Atom of positive
+  | Atom of ident
   | Data32 of Integers.Int.int
   | Data64 of Integers.Int64.int
   | DFreg of freg

backend/Asmexpandaux.mli

@@ -13,7 +13,6 @@
 
 open Asm
 open AST
-open BinNums
 
 (** Auxiliary functions for builtin expansion *)
 
@@ -31,6 +30,6 @@ val set_current_function: coq_function -> unit
   (* Set the current function *)
 val get_current_function: unit -> coq_function
   (* Get the current function *)
-val expand_debug: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
+val expand_debug: ident -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
   (* Expand builtin debug function. Takes the function id, the register number of the stackpointer, a
      function to get the dwarf mapping of varibale names  and for the expansion of simple instructions *)

backend/Cminor.v

@@ -185,29 +185,29 @@ Definition funsig (fd: fundef) :=
 *)
 
 Definition genv := Genv.t fundef unit.
-Definition env := PTree.t val.
+Definition env := ATree.t val.
 
 (** The following functions build the initial local environment at
   function entry, binding parameters to the provided arguments and
   initializing local variables to [Vundef]. *)
 
 Fixpoint set_params (vl: list val) (il: list ident) {struct il} : env :=
   match il, vl with
-  | i1 :: is, v1 :: vs => PTree.set i1 v1 (set_params vs is)
-  | i1 :: is, nil => PTree.set i1 Vundef (set_params nil is)
-  | _, _ => PTree.empty val
+  | i1 :: is, v1 :: vs => ATree.set i1 v1 (set_params vs is)
+  | i1 :: is, nil => ATree.set i1 Vundef (set_params nil is)
+  | _, _ => ATree.empty val
   end.
 
 Fixpoint set_locals (il: list ident) (e: env) {struct il} : env :=
   match il with
   | nil => e
-  | i1 :: is => PTree.set i1 Vundef (set_locals is e)
+  | i1 :: is => ATree.set i1 Vundef (set_locals is e)
   end.
 
 Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=
   match optid with
   | None => e
-  | Some id => PTree.set id v e
+  | Some id => ATree.set id v e
   end.
 
 (** Continuations *)
@@ -359,7 +359,7 @@ Variable m: mem.
 
 Inductive eval_expr: expr -> val -> Prop :=
   | eval_Evar: forall id v,
-      PTree.get id e = Some v ->
+      ATree.get id e = Some v ->
       eval_expr (Evar id) v
   | eval_Econst: forall cst v,
       eval_constant sp cst = Some v ->
@@ -447,7 +447,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_assign: forall f id a k sp e m v,
       eval_expr sp e m a v ->
       step (State f (Sassign id a) k sp e m)
-        E0 (State f Sskip k sp (PTree.set id v e) m)
+        E0 (State f Sskip k sp (ATree.set id v e) m)
 
   | step_store: forall f chunk addr a k sp e m vaddr v m',
       eval_expr sp e m addr vaddr ->
@@ -673,7 +673,7 @@ with exec_stmt:
   | exec_Sassign:
       forall f sp e m id a v,
       eval_expr ge sp e m a v ->
-      exec_stmt f sp e m (Sassign id a) E0 (PTree.set id v e) m Out_normal
+      exec_stmt f sp e m (Sassign id a) E0 (ATree.set id v e) m Out_normal
   | exec_Sstore:
       forall f sp e m chunk addr a vaddr v m',
       eval_expr ge sp e m addr vaddr ->
@@ -948,7 +948,7 @@ Proof.
   constructor.
 
 (* assign *)
-  exists (State f Sskip k sp (PTree.set id v e) m); split.
+  exists (State f Sskip k sp (ATree.set id v e) m); split.
   apply star_one. constructor. auto.
   constructor.
 

backend/CminorSel.v

@@ -165,7 +165,7 @@ Variable m: mem.
 
 Inductive eval_expr: letenv -> expr -> val -> Prop :=
   | eval_Evar: forall le id v,
-      PTree.get id e = Some v ->
+      ATree.get id e = Some v ->
       eval_expr le (Evar id) v
   | eval_Eop: forall le op al vl v,
       eval_exprlist le al vl ->
@@ -284,7 +284,7 @@ End EVAL_EXPR.
 
 Definition set_builtin_res (res: builtin_res ident) (v: val) (e: env) : env :=
   match res with
-  | BR id => PTree.set id v e
+  | BR id => ATree.set id v e
   | _ => e
   end.
 
@@ -348,7 +348,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | step_assign: forall f id a k sp e m v,
       eval_expr sp e m nil a v ->
       step (State f (Sassign id a) k sp e m)
-        E0 (State f Sskip k sp (PTree.set id v e) m)
+        E0 (State f Sskip k sp (ATree.set id v e) m)
 
   | step_store: forall f chunk addr al b k sp e m vl v vaddr m',
       eval_exprlist sp e m nil al vl ->

backend/Debugvar.v

@@ -74,7 +74,7 @@ Fixpoint set_state (v: ident) (i: debuginfo) (s: avail) : avail :=
   match s with
   | nil => (v, i) :: nil
   | (v', i') as vi' :: s' =>
-      match Pos.compare v v' with
+      match Ident.compare v v' with
       | Eq => (v, i) :: s'
       | Lt => (v, i) :: s
       | Gt => vi' :: set_state v i s'
@@ -85,7 +85,7 @@ Fixpoint remove_state (v: ident) (s: avail) : avail :=
   match s with
   | nil => nil
   | (v', i') as vi' :: s' =>
-      match Pos.compare v v' with
+      match Ident.compare v v' with
       | Eq => s'
       | Lt => s
       | Gt => vi' :: remove_state v s'
@@ -157,7 +157,7 @@ Fixpoint join (s1: avail) (s2: avail) {struct s1} : avail :=
         match s2 with
         | nil => nil
         | (v2, i2) as vi2 :: s2' =>
-            match Pos.compare v1 v2 with
+            match Ident.compare v1 v2 with
             | Eq => if eq_debuginfo i1 i2 then vi1 :: join s1' s2' else join s1' s2'
             | Lt => join s1' s2
             | Gt => join2 s2'
@@ -296,7 +296,7 @@ Fixpoint diff (s1 s2: avail) {struct s1} : avail :=
         match s2 with
         | nil => s1
         | (v2, i2) :: s2' =>
-            match Pos.compare v1 v2 with
+            match Ident.compare v1 v2 with
             | Eq => if eq_debuginfo i1 i2 then diff s1' s2' else vi1 :: diff s1' s2'
             | Lt => vi1 :: diff s1' s2
             | Gt => diff2 s2'

backend/Debugvarproof.v

@@ -41,7 +41,8 @@ Remark diff_same:
 Proof.
   induction s as [ | [v i] s]; simpl.
   auto.
-  rewrite Pos.compare_refl. rewrite dec_eq_true. auto.
+  destruct (Ident.compare_spec v v); try solve [eelim Ident.lt_not_eq; eauto].
+  rewrite dec_eq_true. auto.
 Qed.
 
 Remark delta_state_same:
@@ -117,7 +118,7 @@ Qed.
     but establish some confidence in the availability analysis. *)
 
 Definition avail_above (v: ident) (s: avail) : Prop :=
-  forall v' i', In (v', i') s -> Plt v v'.
+  forall v' i', In (v', i') s -> Ident.lt v v'.
 
 Inductive wf_avail: avail -> Prop :=
   | wf_avail_nil:
@@ -132,7 +133,7 @@ Lemma set_state_1:
 Proof.
   induction s as [ | [v' i'] s]; simpl.
 - auto.
-- destruct (Pos.compare v v'); simpl; auto.
+- destruct (Ident.compare v v'); simpl; auto.
 Qed.
 
 Lemma set_state_2:
@@ -141,7 +142,7 @@ Lemma set_state_2:
 Proof.
   induction s as [ | [v1 i1] s]; simpl; intros.
 - contradiction.
-- destruct (Pos.compare_spec v v1); simpl.
+- destruct (Ident.compare_spec v v1); simpl.
 + subst v1. destruct H0. congruence. auto.
 + auto.
 + destruct H0; auto.
@@ -155,14 +156,14 @@ Lemma set_state_3:
 Proof.
   induction 1; simpl; intros.
 - intuition congruence.
-- destruct (Pos.compare_spec v v0); simpl in H1.
+- destruct (Ident.compare_spec v v0); simpl in H1.
 + subst v0. destruct H1. inv H1; auto. right; split.
-  apply not_eq_sym. apply Plt_ne. eapply H; eauto.
+  apply not_eq_sym. apply Ident.lt_not_eq. eapply H; eauto.
   auto.
 + destruct H1. inv H1; auto.
-  destruct H1. inv H1. right; split; auto. apply not_eq_sym. apply Plt_ne. auto.
-  right; split; auto. apply not_eq_sym. apply Plt_ne. apply Plt_trans with v0; eauto.
-+ destruct H1. inv H1. right; split; auto. apply Plt_ne. auto.
+  destruct H1. inv H1. right; split; auto. apply not_eq_sym. apply Ident.lt_not_eq. auto.
+  right; split; auto. apply not_eq_sym. apply Ident.lt_not_eq. apply Ident.lt_trans with v0; eauto.
++ destruct H1. inv H1. right; split; auto. apply Ident.lt_not_eq. auto.
   destruct IHwf_avail as [A | [A B]]; auto.
 Qed.
 
@@ -171,11 +172,11 @@ Lemma wf_set_state:
 Proof.
   induction 1; simpl.
 - constructor. red; simpl; tauto. constructor.
-- destruct (Pos.compare_spec v v0).
+- destruct (Ident.compare_spec v v0).
 + subst v0. constructor; auto.
 + constructor.
   red; simpl; intros. destruct H2.
-  inv H2. auto. apply Plt_trans with v0; eauto.
+  inv H2. auto. apply Ident.lt_trans with v0; eauto.
   constructor; auto.
 + constructor.
   red; intros. exploit set_state_3. eexact H0. eauto. intros [[A B] | [A B]]; subst; eauto.
@@ -187,19 +188,19 @@ Lemma remove_state_1:
 Proof.
   induction 1; simpl; red; intros.
 - auto.
-- destruct (Pos.compare_spec v v0); simpl in *.
-+ subst v0. elim (Plt_strict v); eauto.
-+ destruct H1. inv H1.  elim (Plt_strict v); eauto.
-  elim (Plt_strict v). apply Plt_trans with v0; eauto.
-+ destruct H1. inv H1. elim (Plt_strict v); eauto.  tauto.
+- destruct (Ident.compare_spec v v0); simpl in *.
++ subst v0. elim (Ident.lt_not_eq v v); eauto.
++ destruct H1. inv H1.  elim (Ident.lt_not_eq v v); eauto.
+  elim (Ident.lt_not_eq v v); eauto. apply Ident.lt_trans with v0; eauto.
++ destruct H1. inv H1. elim (Ident.lt_not_eq v v); eauto.  tauto.
 Qed.
 
 Lemma remove_state_2:
   forall v v' i' s, v' <> v -> In (v', i') s -> In (v', i') (remove_state v s).
 Proof.
   induction s as [ | [v1 i1] s]; simpl; intros.
 - auto.
-- destruct (Pos.compare_spec v v1); simpl.
+- destruct (Ident.compare_spec v v1); simpl.
 + subst v1. destruct H0. congruence. auto.
 + auto.
 + destruct H0; auto.
@@ -210,11 +211,11 @@ Lemma remove_state_3:
 Proof.
   induction 1; simpl; intros.
 - contradiction.
-- destruct (Pos.compare_spec v v0); simpl in H1.
-+ subst v0. split; auto. apply not_eq_sym; apply Plt_ne; eauto.
-+ destruct H1. inv H1. split; auto. apply not_eq_sym; apply Plt_ne; eauto.
-  split; auto. apply not_eq_sym; apply Plt_ne. apply Plt_trans with v0; eauto.
-+ destruct H1. inv H1. split; auto. apply Plt_ne; auto.
+- destruct (Ident.compare_spec v v0); simpl in H1.
++ subst v0. split; auto. apply not_eq_sym; apply Ident.lt_not_eq; eauto.
++ destruct H1. inv H1. split; auto. apply not_eq_sym; apply Ident.lt_not_eq; eauto.
+  split; auto. apply not_eq_sym; apply Ident.lt_not_eq. apply Ident.lt_trans with v0; eauto.
++ destruct H1. inv H1. split; auto. apply Ident.lt_not_eq; auto.
   destruct IHwf_avail as [A B] ; auto.
 Qed.
 
@@ -223,7 +224,7 @@ Lemma wf_remove_state:
 Proof.
   induction 1; simpl.
 - constructor.
-- destruct (Pos.compare_spec v v0).
+- destruct (Ident.compare_spec v v0).
 + auto.
 + constructor; auto.
 + constructor; auto. red; intros.
@@ -246,12 +247,22 @@ Lemma join_1:
 Proof.
   induction 1; simpl; try tauto; induction 1; simpl; intros I1 I2; auto.
   destruct I1, I2.
-- inv H3; inv H4. rewrite Pos.compare_refl. rewrite dec_eq_true; auto with coqlib.
+- inv H3; inv H4.
+  destruct (Ident.compare_spec v v); try solve [eelim Ident.lt_not_eq; eauto].
+  rewrite dec_eq_true; auto with coqlib.
 - inv H3.
-  assert (L: Plt v1 v) by eauto. apply Pos.compare_gt_iff in L. rewrite L. auto.
+  assert (L: Ident.lt v1 v) by eauto.
+  destruct (Ident.compare_spec v v1).
+  + eelim Ident.lt_not_eq; eauto.
+  + elim (Ident.lt_not_eq v v); eauto using Ident.lt_trans.
+  + auto.
 - inv H4.
-  assert (L: Plt v0 v) by eauto. apply Pos.compare_lt_iff in L. rewrite L. apply IHwf_avail. constructor; auto. auto. auto with coqlib.
-- destruct (Pos.compare v0 v1).
+  assert (L: Ident.lt v0 v) by eauto.
+  destruct (Ident.compare_spec v0 v).
+  + eelim Ident.lt_not_eq; eauto.
+  + apply IHwf_avail. constructor; auto. auto. auto with coqlib.
+  + elim (Ident.lt_not_eq v v); eauto using Ident.lt_trans.
+- destruct (Ident.compare v0 v1).
 + destruct (eq_debuginfo i0 i1); auto with coqlib.
 + apply IHwf_avail; auto with coqlib. constructor; auto.
 + eauto.
@@ -262,7 +273,7 @@ Lemma join_2:
   In (v, i) (join s1 s2) -> In (v, i) s1 /\ In (v, i) s2.
 Proof.
   induction 1; simpl; try tauto; induction 1; simpl; intros I; try tauto.
-  destruct (Pos.compare_spec v0 v1).
+  destruct (Ident.compare_spec v0 v1).
 - subst v1. destruct (eq_debuginfo i0 i1).
   + subst i1. destruct I. auto. exploit IHwf_avail; eauto. tauto.
   + exploit IHwf_avail; eauto. tauto.
@@ -275,7 +286,7 @@ Lemma wf_join:
   forall s1, wf_avail s1 -> forall s2, wf_avail s2 -> wf_avail (join s1 s2).
 Proof.
   induction 1; simpl; induction 1; simpl; try constructor.
-  destruct (Pos.compare_spec v v0).
+  destruct (Ident.compare_spec v v0).
 - subst v0. destruct (eq_debuginfo i i0); auto. constructor; auto.
   red; intros. apply join_2 in H3; auto. destruct H3. eauto.
 - apply IHwf_avail. constructor; auto.