aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/Clightdefs.v101
-rw-r--r--exportclight/Clightgen.ml9
-rw-r--r--exportclight/ExportClight.ml35
3 files changed, 128 insertions, 17 deletions
diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 83d82d88..c2b38a92 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -15,7 +15,7 @@
(** All imports and definitions used by .v Clight files generated by clightgen *)
-From Coq Require Import String List ZArith.
+From Coq Require Import Ascii String List ZArith.
From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight.
Definition tvoid := Tvoid.
@@ -80,3 +80,102 @@ Definition mkprogram (types: list composite_definition)
prog_types := types;
prog_comp_env := ce;
prog_comp_env_eq := EQ |}.
+
+(** The following encoding of character strings as positive numbers
+ must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
+
+Definition append_bit_pos (b: bool) (p: positive) : positive :=
+ if b then xI p else xO p.
+
+Definition append_char_pos_default (c: ascii) (p: positive) : positive :=
+ let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in
+ xI (xI (xI (xI (xI (xI
+ (append_bit_pos b0 (append_bit_pos b1
+ (append_bit_pos b2 (append_bit_pos b3
+ (append_bit_pos b4 (append_bit_pos b5
+ (append_bit_pos b6 (append_bit_pos b7 p))))))))))))).
+
+Definition append_char_pos (c: ascii) (p: positive) : positive :=
+ match c with
+ | "0"%char => xO (xO (xO (xO (xO (xO p)))))
+ | "1"%char => xI (xO (xO (xO (xO (xO p)))))
+ | "2"%char => xO (xI (xO (xO (xO (xO p)))))
+ | "3"%char => xI (xI (xO (xO (xO (xO p)))))
+ | "4"%char => xO (xO (xI (xO (xO (xO p)))))
+ | "5"%char => xI (xO (xI (xO (xO (xO p)))))
+ | "6"%char => xO (xI (xI (xO (xO (xO p)))))
+ | "7"%char => xI (xI (xI (xO (xO (xO p)))))
+ | "8"%char => xO (xO (xO (xI (xO (xO p)))))
+ | "9"%char => xI (xO (xO (xI (xO (xO p)))))
+ | "a"%char => xO (xI (xO (xI (xO (xO p)))))
+ | "b"%char => xI (xI (xO (xI (xO (xO p)))))
+ | "c"%char => xO (xO (xI (xI (xO (xO p)))))
+ | "d"%char => xI (xO (xI (xI (xO (xO p)))))
+ | "e"%char => xO (xI (xI (xI (xO (xO p)))))
+ | "f"%char => xI (xI (xI (xI (xO (xO p)))))
+ | "g"%char => xO (xO (xO (xO (xI (xO p)))))
+ | "h"%char => xI (xO (xO (xO (xI (xO p)))))
+ | "i"%char => xO (xI (xO (xO (xI (xO p)))))
+ | "j"%char => xI (xI (xO (xO (xI (xO p)))))
+ | "k"%char => xO (xO (xI (xO (xI (xO p)))))
+ | "l"%char => xI (xO (xI (xO (xI (xO p)))))
+ | "m"%char => xO (xI (xI (xO (xI (xO p)))))
+ | "n"%char => xI (xI (xI (xO (xI (xO p)))))
+ | "o"%char => xO (xO (xO (xI (xI (xO p)))))
+ | "p"%char => xI (xO (xO (xI (xI (xO p)))))
+ | "q"%char => xO (xI (xO (xI (xI (xO p)))))
+ | "r"%char => xI (xI (xO (xI (xI (xO p)))))
+ | "s"%char => xO (xO (xI (xI (xI (xO p)))))
+ | "t"%char => xI (xO (xI (xI (xI (xO p)))))
+ | "u"%char => xO (xI (xI (xI (xI (xO p)))))
+ | "v"%char => xI (xI (xI (xI (xI (xO p)))))
+ | "w"%char => xO (xO (xO (xO (xO (xI p)))))
+ | "x"%char => xI (xO (xO (xO (xO (xI p)))))
+ | "y"%char => xO (xI (xO (xO (xO (xI p)))))
+ | "z"%char => xI (xI (xO (xO (xO (xI p)))))
+ | "A"%char => xO (xO (xI (xO (xO (xI p)))))
+ | "B"%char => xI (xO (xI (xO (xO (xI p)))))
+ | "C"%char => xO (xI (xI (xO (xO (xI p)))))
+ | "D"%char => xI (xI (xI (xO (xO (xI p)))))
+ | "E"%char => xO (xO (xO (xI (xO (xI p)))))
+ | "F"%char => xI (xO (xO (xI (xO (xI p)))))
+ | "G"%char => xO (xI (xO (xI (xO (xI p)))))
+ | "H"%char => xI (xI (xO (xI (xO (xI p)))))
+ | "I"%char => xO (xO (xI (xI (xO (xI p)))))
+ | "J"%char => xI (xO (xI (xI (xO (xI p)))))
+ | "K"%char => xO (xI (xI (xI (xO (xI p)))))
+ | "L"%char => xI (xI (xI (xI (xO (xI p)))))
+ | "M"%char => xO (xO (xO (xO (xI (xI p)))))
+ | "N"%char => xI (xO (xO (xO (xI (xI p)))))
+ | "O"%char => xO (xI (xO (xO (xI (xI p)))))
+ | "P"%char => xI (xI (xO (xO (xI (xI p)))))
+ | "Q"%char => xO (xO (xI (xO (xI (xI p)))))
+ | "R"%char => xI (xO (xI (xO (xI (xI p)))))
+ | "S"%char => xO (xI (xI (xO (xI (xI p)))))
+ | "T"%char => xI (xI (xI (xO (xI (xI p)))))
+ | "U"%char => xO (xO (xO (xI (xI (xI p)))))
+ | "V"%char => xI (xO (xO (xI (xI (xI p)))))
+ | "W"%char => xO (xI (xO (xI (xI (xI p)))))
+ | "X"%char => xI (xI (xO (xI (xI (xI p)))))
+ | "Y"%char => xO (xO (xI (xI (xI (xI p)))))
+ | "Z"%char => xI (xO (xI (xI (xI (xI p)))))
+ | "_"%char => xO (xI (xI (xI (xI (xI p)))))
+ | _ => append_char_pos_default c p
+ end.
+
+Fixpoint ident_of_string (s: string) : ident :=
+ match s with
+ | EmptyString => xH
+ | String c s => append_char_pos c (ident_of_string s)
+ end.
+
+(** A convenient notation [$ "ident"] to force evaluation of
+ [ident_of_string "ident"] *)
+
+Ltac ident_of_string s :=
+ let x := constr:(ident_of_string s) in
+ let y := eval compute in x in
+ exact y.
+
+Notation "$ s" := (ltac:(ident_of_string s))
+ (at level 1, only parsing) : string_scope.
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index f7279a5e..637454f0 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -98,6 +98,8 @@ Recognized source files:
.i or .p C source file that should not be preprocessed
Processing options:
-normalize Normalize the generated Clight code w.r.t. loads in expressions
+ -canonical-idents Use canonical numbers to represent identifiers (default)
+ -short-idents Use canonical numbers to represent identifiers
-E Preprocess only, send result to standard output
-o <file> Generate output in <file>
|} ^
@@ -142,6 +144,8 @@ let cmdline_actions =
(* Processing options *)
[ Exact "-E", Set option_E;
Exact "-normalize", Set option_normalize;
+ Exact "-canonical-idents", Set Camlcoq.use_canonical_atoms;
+ Exact "-short-idents", Unset Camlcoq.use_canonical_atoms;
Exact "-o", String(fun s -> option_o := Some s);
Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in
option_o := Some s);]
@@ -175,12 +179,13 @@ let cmdline_actions =
]
let _ =
- try
+try
Gc.set { (Gc.get()) with
Gc.minor_heap_size = 524288; (* 512k *)
Gc.major_heap_increment = 4194304 (* 4M *)
};
Printexc.record_backtrace true;
+ Camlcoq.use_canonical_atoms := true;
Frontend.init ();
parse_cmdline cmdline_actions;
if !option_o <> None && !num_input_files >= 2 then
@@ -188,7 +193,7 @@ let _ =
if !num_input_files = 0 then
fatal_error no_loc "no input file";
perform_actions ()
- with
+with
| Sys_error msg
| CmdError msg -> error no_loc "%s" msg; exit 2
| Abort -> exit 2
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index c9d6fced..87956b58 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -81,8 +81,12 @@ let define_idents p =
string_of_atom
(fun (id, name) ->
try
- fprintf p "Definition _%s : ident := %ld%%positive.@ "
- (sanitize name) (P.to_int32 id)
+ if id = pos_of_string name then
+ fprintf p "Definition _%s : ident := $\"%s\".@ "
+ (sanitize name) name
+ else
+ fprintf p "Definition _%s : ident := %ld%%positive.@ "
+ (sanitize name) (P.to_int32 id)
with Not_an_identifier ->
());
iter_hashtbl_sorted
@@ -93,9 +97,11 @@ let define_idents p =
fprintf p "@ "
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))
+ if not (Hashtbl.mem string_of_atom t) && not (Hashtbl.mem temp_names t)
+ then begin
+ let t1 = P.to_int t and t0 = P.to_int (first_unused_ident ()) in
+ Hashtbl.add temp_names t (sprintf "_t'%d" (t1 - t0 + 1))
+ end
let name_opt_temporary = function
| None -> ()
@@ -468,7 +474,7 @@ let print_assertion p (txt, targs) =
| Text _ -> ()
| Param n -> max_param := max n !max_param)
frags;
- fprintf p " | \"%s\"%%string, " txt;
+ fprintf p " | \"%s\", " txt;
list_iteri
(fun i targ -> fprintf p "_x%d :: " (i + 1))
targs;
@@ -495,7 +501,8 @@ let print_assertions p =
let prologue = "\
From Coq Require Import String List ZArith.\n\
From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\
-Local Open Scope Z_scope.\n"
+Local Open Scope Z_scope.\n\
+Local Open Scope string_scope.\n"
(* Naming the compiler-generated temporaries occurring in the program *)
@@ -554,15 +561,15 @@ let name_program p =
let print_clightgen_info p sourcefile normalized =
fprintf p "@[<v 2>Module Info.";
- fprintf p "@ Definition version := %S%%string." Version.version;
- fprintf p "@ Definition build_number := %S%%string." Version.buildnr;
- fprintf p "@ Definition build_tag := %S%%string." Version.tag;
- fprintf p "@ Definition arch := %S%%string." Configuration.arch;
- fprintf p "@ Definition model := %S%%string." Configuration.model;
- fprintf p "@ Definition abi := %S%%string." Configuration.abi;
+ fprintf p "@ Definition version := %S." Version.version;
+ fprintf p "@ Definition build_number := %S." Version.buildnr;
+ fprintf p "@ Definition build_tag := %S." Version.tag;
+ fprintf p "@ Definition arch := %S." Configuration.arch;
+ fprintf p "@ Definition model := %S." Configuration.model;
+ fprintf p "@ Definition abi := %S." Configuration.abi;
fprintf p "@ Definition bitsize := %d." (if Archi.ptr64 then 64 else 32);
fprintf p "@ Definition big_endian := %B." Archi.big_endian;
- fprintf p "@ Definition source_file := %S%%string." sourcefile;
+ fprintf p "@ Definition source_file := %S." sourcefile;
fprintf p "@ Definition normalized := %B." normalized;
fprintf p "@]@ End Info.@ @ "
generated by cgit (git 2.34.1) at 2024-05-20 05:39:01 +0000