Make ident an abstract type

AST.ident values can now only be created through Ident.of_string, and
can only be used through Ident.to_string. This guarantees that the
concrete positive <-> string mapping used is immaterial and that ident
values can never be communicated with the outside world.

This discipline is enforced both in the Coq and Ocaml code: the
Camlcoq functions intern_string and extern_atom now use the sealed
Ident module (and type) as extracted from Coq. Independently, the
FastIdent Ocaml module provides the string interning backend necessary
for Symbols.v, but it cannot be used to bypass abstraction.

The new structure also makes it easy to switch out the implementation
of the Ident module in the future, or provide an alternative one, for
instance if we want to implement a version of Ident where of_string
and to_string can compute within Coq, sacrificing performance.

Author: jeremie-koenig

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.