Drop uninterned symbols

Instead, we use regular symbols, but make sure that they are not legal
C identifiers, so that they cannot conflict with those parsed from the
source program. Specifically, the temporaries introduced by the
SimplExpr pass are of the form "$1", "$2", etc. (which is similar in
effect to the old behavior when they are printed out), and temporaries
introduced to separate memory loads in clightgen normalization are of
the form "@1", "@2", etc.

Author: jeremie-koenig

cfrontend/SimplExpr.v

@@ -30,10 +30,14 @@ Local Open Scope string_scope.
 (** State and error monad for generating fresh identifiers. *)
 
 Record generator : Type := mkgenerator {
-  gen_next: ident;
+  gen_next: positive;
   gen_trail: list (ident * type)
 }.
 
+(** The ML code prints out the nth reserved identifier as "$n". *)
+Parameter string_of_resid : positive -> String.string.
+Axiom string_of_resid_inj : forall x y, string_of_resid x = string_of_resid y -> x = y.
+
 Inductive result (A: Type) (g: generator) : Type :=
   | Err: Errors.errmsg -> result A g
   | Res: A -> forall (g': generator), Ple (gen_next g) (gen_next g') -> result A g.
@@ -72,15 +76,13 @@ Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
 
 Local Open Scope gensym_monad_scope.
 
-Parameter first_unused_ident: unit -> ident.
-
 Definition initial_generator (x: unit) : generator :=
-  mkgenerator (first_unused_ident x) nil.
+  mkgenerator 1%positive nil.
 
 Definition gensym (ty: type): mon ident :=
   fun (g: generator) =>
-    Res (gen_next g)
-        (mkgenerator (Pos.succ (gen_next g)) ((gen_next g, ty) :: gen_trail g))
+    Res #(string_of_resid (gen_next g))
+        (mkgenerator (Pos.succ (gen_next g)) ((#(string_of_resid (gen_next g)), ty) :: gen_trail g))
         (Ple_succ (gen_next g)).
 
 (** Construct a sequence from a list of statements.  To facilitate the

cfrontend/SimplExprspec.v

@@ -555,13 +555,17 @@ Ltac monadInv H :=
 (** ** Freshness and separation properties. *)
 
 Definition within (id: ident) (g1 g2: generator) : Prop :=
-  Ple (gen_next g1) id /\ Plt id (gen_next g2).
+  exists p,
+    id = #(string_of_resid p) /\
+    Ple (gen_next g1) p /\ Plt p (gen_next g2).
 
 Lemma gensym_within:
   forall ty g1 id g2 I,
   gensym ty g1 = Res id g2 I -> within id g1 g2.
 Proof.
-  intros. monadInv H. split. apply Ple_refl. apply Plt_succ.
+  intros. monadInv H.
+  exists (gen_next g1); intuition idtac.
+  apply Ple_refl. apply Plt_succ.
 Qed.
 
 Lemma within_widen:
@@ -571,7 +575,8 @@ Lemma within_widen:
   Ple (gen_next g2) (gen_next g2') ->
   within id g1' g2'.
 Proof.
-  intros. destruct H. split.
+  intros. destruct H as (? & ? & ?).
+  exists x; intuition idtac.
   eapply Ple_trans; eauto.
   eapply Plt_Ple_trans; eauto.
 Qed.
@@ -609,26 +614,40 @@ Proof.
   intros; red; intros. destruct (in_app_or _ _ _ H1); auto.
 Qed.
 
+Lemma ident_of_string_inj s t:
+  ident_of_string s = ident_of_string t -> s = t.
+Proof.
+  intros Hst.
+  rewrite <- (string_of_ident_of_string s).
+  rewrite <- (string_of_ident_of_string t).
+  congruence.
+Qed.
+
 Lemma contained_disjoint:
   forall g1 l1 g2 l2 g3,
   contained l1 g1 g2 -> contained l2 g2 g3 -> list_disjoint l1 l2.
 Proof.
   intros; red; intros. red; intro; subst y.
-  exploit H; eauto. intros [A B]. exploit H0; eauto. intros [Csyntax D].
-  elim (Plt_strict x). apply Plt_Ple_trans with (gen_next g2); auto.
+  exploit H; eauto. intros (p & Hp & A & B).
+  exploit H0; eauto. intros (q & Hq & Csyntax & D).
+  assert (p = q) by (apply string_of_resid_inj, ident_of_string_inj; congruence).
+  subst q. elim (Plt_strict p). apply Plt_Ple_trans with (gen_next g2); auto.
 Qed.
 
 Lemma contained_notin:
   forall g1 l g2 id g3,
   contained l g1 g2 -> within id g2 g3 -> ~In id l.
 Proof.
-  intros; red; intros. exploit H; eauto. intros [Csyntax D]. destruct H0 as [A B].
-  elim (Plt_strict id). apply Plt_Ple_trans with (gen_next g2); auto.
+  intros; red; intros.
+  exploit H; eauto. intros (p & Hp & Csyntax & D).
+  destruct H0 as (q & Hq & A & B).
+  assert (p = q) by (apply string_of_resid_inj, ident_of_string_inj; congruence).
+  subst q. elim (Plt_strict p). apply Plt_Ple_trans with (gen_next g2); auto.
 Qed.
 
 Definition dest_below (dst: destination) (g: generator) : Prop :=
   match dst with
-  | For_set sd => Plt (sd_temp sd) g.(gen_next)
+  | For_set sd => exists p, sd_temp sd = #(string_of_resid p) /\ Plt p g.(gen_next)
   | _ => True
   end.
 
@@ -642,7 +661,7 @@ Lemma dest_for_set_seqbool_val:
   forall tmp ty g1 g2,
   within tmp g1 g2 -> dest_below (For_set (sd_seqbool_val tmp ty)) g2.
 Proof.
-  intros. destruct H. simpl. auto.
+  intros. destruct H as (p & Hp & A & B). simpl. eauto.
 Qed.
 
 Lemma dest_for_set_seqbool_set:
@@ -654,27 +673,30 @@ Qed.
 Lemma dest_for_set_condition_val:
   forall tmp tycast ty g1 g2, within tmp g1 g2 -> dest_below (For_set (SDbase tycast ty tmp)) g2.
 Proof.
-  intros. destruct H. simpl. auto.
+  intros. destruct H as (p & Hp & A & B). simpl. eauto.
 Qed.
 
 Lemma dest_for_set_condition_set:
   forall sd tmp tycast ty g1 g2, dest_below (For_set sd) g2 -> within tmp g1 g2 -> dest_below (For_set (SDcons tycast ty tmp sd)) g2.
 Proof.
-  intros. destruct H0. simpl. auto.
+  intros. destruct H0 as (p & Hp & A & B). simpl. eauto.
 Qed.
 
 Lemma sd_temp_notin:
   forall sd g1 g2 l, dest_below (For_set sd) g1 -> contained l g1 g2 -> ~In (sd_temp sd) l.
 Proof.
-  intros. simpl in H. red; intros. exploit H0; eauto. intros [A B].
-  elim (Plt_strict (sd_temp sd)). apply Plt_Ple_trans with (gen_next g1); auto.
+  intros. destruct H as (p & Hp & H). red; intros.
+  exploit H0; eauto. intros (q & Hq & A & B).
+  assert (p = q) by (apply string_of_resid_inj, ident_of_string_inj; congruence).
+  subst q. elim (Plt_strict p). apply Plt_Ple_trans with (gen_next g1); auto.
 Qed.
 
 Lemma dest_below_le:
   forall dst g1 g2,
   dest_below dst g1 -> Ple g1.(gen_next) g2.(gen_next) -> dest_below dst g2.
 Proof.
-  intros. destruct dst; simpl in *; auto. eapply Plt_Ple_trans; eauto.
+  intros. destruct dst; simpl in *; auto.
+  destruct H as (p & Hp & H). eauto using Plt_Ple_trans.
 Qed.
 
 Hint Resolve gensym_within within_widen contained_widen

exportclight/Clightnorm.ml

@@ -33,12 +33,12 @@ open Camlcoq
 open Ctypes
 open Clight
 
-let gen_next : AST.ident ref = ref P.one
+let gen_next : int ref = ref 1
 let gen_trail : (AST.ident * coq_type) list ref = ref []
 
 let gensym ty =
-  let id = !gen_next in
-  gen_next := P.succ id;
+  let id = intern_string (Printf.sprintf "@%d" !gen_next) in
+  gen_next := !gen_next + 1;
   gen_trail := (id, ty) :: !gen_trail;
   id
 
@@ -148,10 +148,7 @@ let next_var curr (v, _) = if P.lt v curr then curr else P.succ v
 let next_var_list vars start = List.fold_left next_var start vars
 
 let norm_function f =
-  gen_next := next_var_list f.fn_params
-                (next_var_list f.fn_vars
-                   (next_var_list f.fn_temps
-                     (Camlcoq.first_unused_ident ())));
+  gen_next := 1;
   gen_trail := [];
   let s' = norm_stmt f.fn_body in
   let new_temps = !gen_trail in

extraction/extraction.v

@@ -94,7 +94,7 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc".
 Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
 
 (* SimplExpr *)
-Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident".
+Extract Constant SimplExpr.string_of_resid => "Camlcoq.coqstring_of_resid".
 Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2.
 
 (* Compopts *)

lib/Camlcoq.ml

@@ -299,7 +299,7 @@ let next_temp = ref 1
 
 let rec fresh_temp () =
   assert (!next_temp != 0);
-  let s = Printf.sprintf "$%d" !next_temp in
+  let s = Printf.sprintf "!%d" !next_temp in
   next_temp := !next_temp + 1;
   if Hashtbl.mem atom_of_string s then fresh_temp () else s
 
@@ -322,8 +322,6 @@ let extern_atom a =
     Hashtbl.add string_of_atom a s;
     s
 
-let first_unused_ident () = !next_atom
-
 (* Strings *)
 
 let camlstring_of_coqstring (s: char list) =
@@ -352,6 +350,8 @@ let ident_of_coqstring s =
   intern_string (camlstring_of_coqstring s)
 let coqstring_of_ident a =
   coqstring_of_camlstring (extern_atom a)
+let coqstring_of_resid p =
+  coqstring_of_camlstring (Printf.sprintf "$%d" (P.to_int p))
 
 (* Floats *)