diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Camlcoq.ml | 79 | ||||
-rw-r--r-- | lib/Commandline.ml | 141 | ||||
-rw-r--r-- | lib/Commandline.mli | 55 | ||||
-rw-r--r-- | lib/Floats.v | 4 | ||||
-rw-r--r-- | lib/IEEE754_extra.v | 4 | ||||
-rw-r--r-- | lib/Readconfig.mll | 2 | ||||
-rw-r--r-- | lib/Zbits.v | 4 |
7 files changed, 279 insertions, 10 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 66322efb..af65b28e 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -282,23 +282,96 @@ type atom = positive let atom_of_string = (Hashtbl.create 17 : (string, atom) Hashtbl.t) let string_of_atom = (Hashtbl.create 17 : (atom, string) Hashtbl.t) let next_atom = ref Coq_xH +let use_canonical_atoms = ref false + +(* If [use_canonical_atoms] is false, strings are numbered from 1 up + in the order in which they are encountered. This produces small + numbers, and is therefore efficient, but the number for a given + string may differ between the compilation of different units. + + If [use_canonical_atoms] is true, strings are Huffman-encoded as bit + sequences, which are then encoded as positive numbers. The same + string is always represented by the same number in all compilation + units. However, the numbers are bigger than in the first + implementation. Also, this places a hard limit on the number of + fresh identifiers that can be generated starting with + [first_unused_ident]. *) + +let rec append_bits_pos nbits n p = + if nbits <= 0 then p else + if n land 1 = 0 + then Coq_xO (append_bits_pos (nbits - 1) (n lsr 1) p) + else Coq_xI (append_bits_pos (nbits - 1) (n lsr 1) p) + +(* The encoding of strings as bit sequences is optimized for C identifiers: + - numbers are encoded as a 6-bit integer between 0 and 9 + - lowercase letters are encoded as a 6-bit integer between 10 and 35 + - uppercase letters are encoded as a 6-bit integer between 36 and 61 + - the underscore character is encoded as the 6-bit integer 62 + - all other characters are encoded as 6 "one" bits followed by + the 8-bit encoding of the character. *) + +let append_char_pos c p = + match c with + | '0'..'9' -> append_bits_pos 6 (Char.code c - Char.code '0') p + | 'a'..'z' -> append_bits_pos 6 (Char.code c - Char.code 'a' + 10) p + | 'A'..'Z' -> append_bits_pos 6 (Char.code c - Char.code 'A' + 36) p + | '_' -> append_bits_pos 6 62 p + | _ -> append_bits_pos 6 63 (append_bits_pos 8 (Char.code c) p) + +(* The empty string is represented as the positive "1", that is, [xH]. *) + +let pos_of_string s = + let rec encode i accu = + if i < 0 then accu else encode (i - 1) (append_char_pos s.[i] accu) + in encode (String.length s - 1) Coq_xH + +let fresh_atom () = + let a = !next_atom in + next_atom := Pos.succ !next_atom; + a let intern_string s = try Hashtbl.find atom_of_string s with Not_found -> - let a = !next_atom in - next_atom := Pos.succ !next_atom; + let a = + if !use_canonical_atoms then pos_of_string s else fresh_atom () in Hashtbl.add atom_of_string s a; Hashtbl.add string_of_atom a s; a + let extern_atom a = try Hashtbl.find string_of_atom a with Not_found -> Printf.sprintf "$%d" (P.to_int a) -let first_unused_ident () = !next_atom +(* Ignoring the terminating "1" bit, canonical encodings of strings can + be viewed as lists of bits, formed by concatenation of 6-bit fragments + (for letters, numbers, and underscore) and 14-bit fragments (for other + characters). Hence, not all positive numbers are canonical encodings: + only those whose log2 is of the form [6n + 14m]. + + Here are the first intervals of positive numbers corresponding to strings: + - [1, 1] for the empty string + - [2^6, 2^7-1] for one "compact" character + - [2^12, 2^13-1] for two "compact" characters + - [2^14, 2^14-1] for one "escaped" character + + Hence, between 2^7 and 2^12 - 1, we have 3968 consecutive positive + numbers that cannot be the encoding of a string. These are the positive + numbers we'll use as temporaries in the SimplExpr pass if canonical + atoms are in use. + + If short atoms are used, we just number the temporaries consecutively + starting one above the last generated atom. +*) + +let first_unused_ident () = + if !use_canonical_atoms + then P.of_int 128 + else !next_atom (* Strings *) diff --git a/lib/Commandline.ml b/lib/Commandline.ml new file mode 100644 index 00000000..672ed834 --- /dev/null +++ b/lib/Commandline.ml @@ -0,0 +1,141 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Parsing of command-line flags and arguments *) + +open Printf + +type pattern = + | Exact of string + | Prefix of string + | Suffix of string + | Regexp of Str.regexp + +let _Regexp re = Regexp (Str.regexp re) + +type action = + | Set of bool ref + | Unset of bool ref + | Self of (string -> unit) + | String of (string -> unit) + | Integer of (int -> unit) + | Ignore + | Unit of (unit -> unit) + +exception CmdError of string + +let match_pattern text = function + | Exact s -> + text = s + | Prefix pref -> + let lpref = String.length pref and ltext = String.length text in + lpref < ltext && String.sub text 0 lpref = pref + (* strict prefix: no match if pref = text. See below. *) + | Suffix suff -> + let lsuff = String.length suff and ltext = String.length text in + lsuff < ltext && String.sub text (ltext - lsuff) lsuff = suff + (* strict suffix: no match if suff = text, so that e.g. ".c" + causes an error rather than being treated as a C source file. *) + | Regexp re -> + Str.string_match re text 0 + +let rec find_action text = function + | [] -> None + | (pat, act) :: rem -> + if match_pattern text pat then Some act else find_action text rem + +let parse_array spec argv first last = + (* Split the spec into Exact patterns (in a hashtable) and other patterns *) + let exact_cases = (Hashtbl.create 29 : (string, action) Hashtbl.t) in + let rec split_spec = function + | [] -> [] + | (Exact s, act) :: rem -> Hashtbl.add exact_cases s act; split_spec rem + | (pat, act) :: rem -> (pat, act) :: split_spec rem in + let inexact_cases = split_spec spec in + (* Parse the vector of arguments *) + let rec parse i = + if i <= last then begin + let s = argv.(i) in + let optact = + try Some (Hashtbl.find exact_cases s) + with Not_found -> find_action s inexact_cases in + match optact with + | None -> + let msg = sprintf "unknown argument `%s'" s in + raise (CmdError msg) + | Some(Set r) -> + r := true; parse (i+1) + | Some(Unset r) -> + r := false; parse (i+1) + | Some(Self fn) -> + fn s; parse (i+1) + | Some(String fn) -> + if i + 1 <= last then begin + fn argv.(i+1); parse (i+2) + end else begin + let msg = sprintf "option `%s' expects an argument" s in + raise (CmdError msg) + end + | Some(Integer fn) -> + if i + 1 <= last then begin + let n = + try + int_of_string argv.(i+1) + with Failure _ -> + let msg = sprintf "argument to option `%s' must be an integer" s in + raise (CmdError msg) + in + fn n; parse (i+2) + end else begin + let msg = sprintf "option `%s' expects an argument" s in + raise (CmdError msg) + end + | Some (Ignore) -> + if i + 1 <= last then begin + parse (i+2) + end else begin + let msg = sprintf "option `%s' expects an argument" s in + raise (CmdError msg) + end + | Some (Unit f) -> f (); parse (i+1) + end + in parse first + +let argv = + try + Responsefile.expandargv Sys.argv + with Responsefile.Error msg | Sys_error msg -> + eprintf "Error while processing the command line: %s\n" msg; + exit 2 + +let parse_cmdline spec = + parse_array spec argv 1 (Array.length argv - 1) + +let long_int_action key s = + let ls = String.length s + and lkey = String.length key in + assert (ls > lkey); + let s = String.sub s (lkey + 1) (ls - lkey - 1) in + try + int_of_string s + with Failure _ -> + let msg = sprintf "argument to option `%s' must be an integer" key in + raise (CmdError msg) + +let longopt_int key f = + let act s = + let n = long_int_action key s in + f n in + Prefix (key ^ "="),Self act diff --git a/lib/Commandline.mli b/lib/Commandline.mli new file mode 100644 index 00000000..8bb6f18f --- /dev/null +++ b/lib/Commandline.mli @@ -0,0 +1,55 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Parsing of command-line flags and arguments *) + +(* A command-line specification is a list of pairs (pattern, action). + Command-line words are matched against the patterns, and the + corresponding actions are invoked. *) + +type pattern = + | Exact of string (** exactly this string *) + | Prefix of string (** any string starting with this prefix *) + | Suffix of string (** any string ending with this suffix *) + | Regexp of Str.regexp (** any string matching this anchored regexp *) + +val _Regexp: string -> pattern (** text of an [Str] regexp *) + +type action = + | Set of bool ref (** set the given ref to true *) + | Unset of bool ref (** set the given ref to false *) + | Self of (string -> unit) (** call the function with the matched string *) + | String of (string -> unit) (** read next arg as a string, call function *) + | Integer of (int -> unit) (** read next arg as an int, call function *) + | Ignore (** ignore the next arg *) + | Unit of (unit -> unit) (** call the function with unit as argument *) +(* Note on precedence: [Exact] patterns are tried first, then the other + patterns are tried in the order in which they appear in the list. *) + +exception CmdError of string +(** Raise by [parse_cmdline] when an error occurred *) + +val parse_cmdline: (pattern * action) list -> unit +(** [parse_cmdline actions] parses the command line (after @-file expansion) + and performs all [actions]. Raises [CmdError] if an error occurred. +*) + +val longopt_int: string -> (int -> unit) -> pattern * action +(** [longopt_int key fn] generates a pattern and an action for + options of the form [key=<n>] and calls [fn] with the integer argument +*) + +val argv: string array +(** [argv] contains the complete command line after @-file expandsion *) diff --git a/lib/Floats.v b/lib/Floats.v index 272efa52..ac67b88c 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -17,11 +17,11 @@ (** Formalization of floating-point numbers, using the Flocq library. *) Require Import Coqlib Zbits Integers Axioms. -(*From Flocq*) -Require Import Binary Bits Core. +From Flocq Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. Require Archi. +Import ListNotations. Close Scope R_scope. Open Scope Z_scope. diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index c23149be..18313ec1 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -17,11 +17,11 @@ (** Additional operations and proofs about IEEE-754 binary floating-point numbers, on top of the Flocq library. *) +From Flocq Require Import Core Digits Operations Round Bracket Sterbenz + Binary Round_odd. Require Import Psatz. Require Import Bool. Require Import Eqdep_dec. -(*From Flocq *) -Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd. Local Open Scope Z_scope. diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll index 7b98255e..8abcc407 100644 --- a/lib/Readconfig.mll +++ b/lib/Readconfig.mll @@ -20,7 +20,7 @@ let key_val_tbl : (string, string list) Hashtbl.t = Hashtbl.create 17 let key_val key = - try Some(Hashtbl.find key_val_tbl key) with Not_found -> None + Hashtbl.find_opt key_val_tbl key (* Auxiliaries for parsing *) diff --git a/lib/Zbits.v b/lib/Zbits.v index 27586aff..6f3acaab 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -266,7 +266,7 @@ Qed. Remark Ztestbit_shiftin_base: forall b x, Z.testbit (Zshiftin b x) 0 = b. Proof. - intros. rewrite Ztestbit_shiftin. apply zeq_true. omega. + intros. rewrite Ztestbit_shiftin; reflexivity. Qed. Remark Ztestbit_shiftin_succ: @@ -316,7 +316,7 @@ Qed. Remark Ztestbit_base: forall x, Z.testbit x 0 = Z.odd x. Proof. - intros. rewrite Ztestbit_eq. apply zeq_true. omega. + intros. rewrite Ztestbit_eq; reflexivity. Qed. Remark Ztestbit_succ: |