Merge branch 'kvx-work' into aarch64-peephole

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: