diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2016-02-05 13:51:47 +0100 |
---|---|---|
committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2016-02-05 13:51:47 +0100 |
commit | f65abd772e574adf0493336a32fb4ea1fe230a8d (patch) | |
tree | 1b2b2cb5a13f2d97d3e38602622a3f5a0d898b9f | |
parent | abb704f93055a572a5078e04c5212ff051309730 (diff) | |
parent | 03112fe3624762c95bab7606eb8b1a56f6bab3db (diff) | |
download | compcert-f65abd772e574adf0493336a32fb4ea1fe230a8d.tar.gz compcert-f65abd772e574adf0493336a32fb4ea1fe230a8d.zip |
Merge pull request #86 from AbsInt/clightgen-improved
Better treatment of names in the clightgen tool
-rw-r--r-- | cfrontend/SimplExpr.v | 60 | ||||
-rw-r--r-- | cfrontend/SimplExprproof.v | 5 | ||||
-rw-r--r-- | cfrontend/SimplExprspec.v | 31 | ||||
-rw-r--r-- | exportclight/ExportClight.ml | 108 |
4 files changed, 114 insertions, 90 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 4fe8105d..a5a6ad66 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -91,14 +91,6 @@ Definition gensym (ty: type): mon ident := (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g)) (Ple_succ (gen_next g)). -Definition reset_trail: mon unit := - fun (g: generator) => - Res tt (mkgenerator (gen_next g) nil) (Ple_refl (gen_next g)). - -Definition get_trail: mon (list (ident * type)) := - fun (g: generator) => - Res (gen_trail g) g (Ple_refl (gen_next g)). - (** Construct a sequence from a list of statements. To facilitate the proof, the sequence is nested to the left and starts with a [Sskip]. *) @@ -113,7 +105,7 @@ Definition makeseq (l: list statement) : statement := (** Smart constructor for [if ... then ... else]. *) -Function eval_simpl_expr (a: expr) : option val := +Fixpoint eval_simpl_expr (a: expr) : option val := match a with | Econst_int n _ => Some(Vint n) | Econst_float n _ => Some(Vfloat n) @@ -502,49 +494,35 @@ with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements := (** Translation of a function *) -Definition transl_function (f: Csyntax.function) : mon function := - do x <- reset_trail; - do tbody <- transl_stmt f.(Csyntax.fn_body); - do temps <- get_trail; - ret (mkfunction +Definition transl_function (f: Csyntax.function) : res function := + match transl_stmt f.(Csyntax.fn_body) (initial_generator tt) with + | Err msg => + Error msg + | Res tbody g i => + OK (mkfunction f.(Csyntax.fn_return) f.(Csyntax.fn_callconv) f.(Csyntax.fn_params) f.(Csyntax.fn_vars) - temps - tbody). - -Definition transl_fundef (fd: Csyntax.fundef) : mon fundef := - match fd with - | Csyntax.Internal f => - do tf <- transl_function f; ret (Internal tf) - | Csyntax.External ef targs tres cconv => - ret (External ef targs tres cconv) + g.(gen_trail) + tbody) end. Local Open Scope error_monad_scope. -Fixpoint transl_globdefs - (l: list (ident * globdef Csyntax.fundef type)) - (g: generator) : res (list (ident * globdef Clight.fundef type)) := - match l with - | nil => OK nil - | (id, Gfun f) :: l' => - match transl_fundef f g with - | Err msg => - Error (MSG "In function " :: CTX id :: MSG ": " :: msg) - | Res tf g' _ => - do tl' <- transl_globdefs l' g'; OK ((id, Gfun tf) :: tl') - end - | (id, Gvar v) :: l' => - do tl' <- transl_globdefs l' g; OK ((id, Gvar v) :: tl') +Definition transl_fundef (fd: Csyntax.fundef) : res fundef := + match fd with + | Csyntax.Internal f => + do tf <- transl_function f; OK (Internal tf) + | Csyntax.External ef targs tres cc => + OK (External ef targs tres cc) end. Definition transl_program (p: Csyntax.program) : res program := - do gl' <- transl_globdefs (Csyntax.prog_defs p) (initial_generator tt); - OK {| prog_defs := gl'; - prog_public := Csyntax.prog_public p; - prog_main := Csyntax.prog_main p; + do p1 <- AST.transform_partial_program transl_fundef p; + OK {| prog_defs := AST.prog_defs p1; + prog_public := AST.prog_public p1; + prog_main := AST.prog_main p1; prog_types := Csyntax.prog_types p; prog_comp_env := Csyntax.prog_comp_env p; prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}. diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 8f06e777..0c7c9ce7 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -2235,8 +2235,9 @@ Proof. econstructor; split. econstructor. exploit Genv.init_mem_match; eauto. - change (Genv.globalenv tprog) with (genv_genv tge). rewrite symbols_preserved. - rewrite <- H4; simpl; eauto. + change (Genv.globalenv tprog) with (genv_genv tge). + rewrite symbols_preserved. rewrite <- H4; simpl. + rewrite (transform_partial_program_main _ _ EQ). eauto. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 7003c78a..4077d7df 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -1088,7 +1088,8 @@ Opaque transl_expression transl_expr_stmt. monadInv TR; constructor; eauto. Qed. -(** Relational presentation for the transformation of functions, fundefs, and variables. *) +(** Relational presentation for the transformation of functions, fundefs, and va +riables. *) Inductive tr_function: Csyntax.function -> Clight.function -> Prop := | tr_function_intro: forall f tf, @@ -1107,37 +1108,37 @@ Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop := tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv). Lemma transl_function_spec: - forall f tf g g' i, - transl_function f g = Res tf g' i -> + forall f tf, + transl_function f = OK tf -> tr_function f tf. Proof. - unfold transl_function; intros. monadInv H. + unfold transl_function; intros. + destruct (transl_stmt (Csyntax.fn_body f) (initial_generator tt)) eqn:T; inv H. constructor; auto. simpl. eapply transl_stmt_meets_spec; eauto. Qed. Lemma transl_fundef_spec: - forall fd tfd g g' i, - transl_fundef fd g = Res tfd g' i -> + forall fd tfd, + transl_fundef fd = OK tfd -> tr_fundef fd tfd. Proof. unfold transl_fundef; intros. - destruct fd; monadInv H. + destruct fd; Errors.monadInv H. + constructor. eapply transl_function_spec; eauto. + constructor. Qed. Lemma transl_globdefs_spec: - forall l g l', - transl_globdefs l g = OK l' -> + forall l l', + transf_globdefs transl_fundef (fun v : type => OK v) l = OK l' -> list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'. Proof. induction l; simpl; intros. - inv H. constructor. - destruct a as [id gd]. destruct gd. - + destruct (transl_fundef f g) as [? | tf g' ?] eqn:E1; try discriminate. - destruct (transl_globdefs l g') eqn:E2; simpl in H; inv H. + + destruct (transl_fundef f) as [tf | ?] eqn:E1; Errors.monadInv H. constructor; eauto. constructor. eapply transl_fundef_spec; eauto. - + destruct (transl_globdefs l g) eqn:E2; simpl in H; inv H. + + Errors.monadInv H. constructor; eauto. destruct v; constructor; auto. Qed. @@ -1146,9 +1147,9 @@ Theorem transl_program_spec: transl_program p = OK tp -> match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp. Proof. - unfold transl_program; intros. - destruct (transl_globdefs (Csyntax.prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H. - split; auto. exists l; split. eapply transl_globdefs_spec; eauto. + unfold transl_program, transform_partial_program; intros. Errors.monadInv H. Errors.monadInv EQ; simpl. + split; auto. exists x0; split. + eapply transl_globdefs_spec; eauto. rewrite <- app_nil_end; auto. Qed. diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 96c7398f..5d4ab88b 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -60,10 +60,7 @@ let sanitize s = done; s' -module StringSet = Set.Make(String) - let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17 -let all_temp_names : StringSet.t ref = ref StringSet.empty let ident p id = try @@ -76,41 +73,35 @@ let ident p id = with Not_found -> fprintf p "%ld%%positive" (P.to_int32 id) +let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) = + List.iter f + (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2) + (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h [])) + let define_idents p = - Hashtbl.iter - (fun id name -> + iter_hashtbl_sorted + string_of_atom + (fun (id, name) -> try fprintf p "Definition _%s : ident := %ld%%positive.@ " (sanitize name) (P.to_int32 id) with Not_an_identifier -> - ()) - string_of_atom; - Hashtbl.iter - (fun id name -> + ()); + iter_hashtbl_sorted + temp_names + (fun (id, name) -> fprintf p "Definition %s : ident := %ld%%positive.@ " - name (P.to_int32 id)) - temp_names; + name (P.to_int32 id)); fprintf p "@ " -let rec find_temp_name name counter = - let name' = - if counter = 0 then name ^ "'" else sprintf "%s'%d" name counter in - if StringSet.mem name' !all_temp_names - then find_temp_name name (counter + 1) - else name' - -let name_temporary t v = - (* Try to give "t" a name that is the name of "v" with a prime - plus a number to disambiguate if needed. *) - if not (Hashtbl.mem string_of_atom t || Hashtbl.mem temp_names t) then begin - try - let vname = "_" ^ sanitize (Hashtbl.find string_of_atom v) in - let tname = find_temp_name vname 0 in - Hashtbl.add temp_names t tname; - all_temp_names := StringSet.add tname !all_temp_names - with Not_found | Not_an_identifier -> - () - end +let name_temporary t = + let t1 = P.to_int t and t0 = P.to_int (first_unused_ident ()) in + if t1 >= t0 && not (Hashtbl.mem temp_names t) + then Hashtbl.add temp_names t (sprintf "_t'%d" (t1 - t0 + 1)) + +let name_opt_temporary = function + | None -> () + | Some id -> name_temporary id (* Numbers *) @@ -489,13 +480,66 @@ Local Open Scope Z_scope. " +(* Naming the compiler-generated temporaries occurring in the program *) + +let rec name_expr = function + | Evar(id, t) -> () + | Etempvar(id, t) -> name_temporary id + | Ederef(a1, t) -> name_expr a1 + | Efield(a1, f, t) -> name_expr a1 + | Econst_int(n, t) -> () + | Econst_float(n, t) -> () + | Econst_long(n, t) -> () + | Econst_single(n, t) -> () + | Eunop(op, a1, t) -> name_expr a1 + | Eaddrof(a1, t) -> name_expr a1 + | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2 + | Ecast(a1, t) -> name_expr a1 + | Esizeof(t1, t) -> () + | Ealignof(t1, t) -> () + +let rec name_stmt = function + | Sskip -> () + | Sassign(e1, e2) -> name_expr e1; name_expr e2 + | Sset(id, e2) -> name_temporary id; name_expr e2 + | Scall(optid, e1, el) -> + name_opt_temporary optid; name_expr e1; List.iter name_expr el + | Sbuiltin(optid, ef, tyl, el) -> + name_opt_temporary optid; List.iter name_expr el + | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2 + | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2 + | Sloop(s1, s2) -> name_stmt s1; name_stmt s2 + | Sbreak -> () + | Scontinue -> () + | Sswitch(e, cases) -> name_expr e; name_lblstmts cases + | Sreturn (Some e) -> name_expr e + | Sreturn None -> () + | Slabel(lbl, s1) -> name_stmt s1 + | Sgoto lbl -> () + +and name_lblstmts = function + | LSnil -> () + | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls + +let name_function f = + List.iter (fun (id, ty) -> name_temporary id) f.fn_temps; + name_stmt f.fn_body + +let name_globdef (id, g) = + match g with + | Gfun(Internal f) -> name_function f + | _ -> () + +let name_program p = + List.iter name_globdef p.prog_defs + (* All together *) let print_program p prog = + Hashtbl.clear temp_names; + name_program prog; fprintf p "@[<v 0>"; fprintf p "%s" prologue; - Hashtbl.clear temp_names; - all_temp_names := StringSet.empty; define_idents p; List.iter (print_globdef p) prog.prog_defs; fprintf p "Definition composites : list composite_definition :=@ "; |