diff --git a/.Makefile.lint b/.Makefile.lint
index fc916bfa1e33d42ff2e73b588b496e21b2d85da4..c74c7c5be984e086ae376f259a784e7374c0f3e5 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -11,8 +11,6 @@ ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
-ML_LINT_KO+=src/kernel_internals/typing/alpha.ml
-ML_LINT_KO+=src/kernel_internals/typing/alpha.mli
ML_LINT_KO+=src/kernel_internals/typing/asm_contracts.ml
ML_LINT_KO+=src/kernel_internals/typing/cfg.ml
ML_LINT_KO+=src/kernel_internals/typing/cfg.mli
diff --git a/src/kernel_internals/typing/alpha.ml b/src/kernel_internals/typing/alpha.ml
index 66f32b2e3e9cb568e0bd192319d75872c86cef13..727d2c77733d52b85bd88b6e909f69f36e46f6a5 100644
--- a/src/kernel_internals/typing/alpha.ml
+++ b/src/kernel_internals/typing/alpha.ml
@@ -47,16 +47,16 @@ module H = Hashtbl
let alphaSeparator = '_'
(** For each prefix we remember the last integer suffix that has been used
- (to start searching for a fresh name) and the list
- * of suffixes, each with some data associated with the newAlphaName that
+ (to start searching for a fresh name) and the list
+ * of suffixes, each with some data associated with the newAlphaName that
* created the suffix. *)
type 'a alphaTableData = Integer.t * (Integer.t * 'a) list
-type 'a undoAlphaElement =
- AlphaChangedSuffix of 'a alphaTableData ref * 'a alphaTableData (* The
- * reference that was changed and
- * the old suffix *)
- | AlphaAddedSuffix of string * string (* We added this new entry to the
+type 'a undoAlphaElement =
+ AlphaChangedSuffix of 'a alphaTableData ref * 'a alphaTableData (* The
+ * reference that was changed and
+ * the old suffix *)
+ | AlphaAddedSuffix of string * string (* We added this new entry to the
* table *)
type 'a alphaTable = (string, (string, 'a alphaTableData ref) H.t) H.t
@@ -64,11 +64,11 @@ type 'a alphaTable = (string, (string, 'a alphaTableData ref) H.t) H.t
(* specify a behavior for renaming *)
type rename_mode =
| Incr_last_suffix
- (* increment the last suffix in the original id
- (adding _nnn if no suffix exists in the original id) *)
+ (* increment the last suffix in the original id
+ (adding _nnn if no suffix exists in the original id) *)
| Add_new_suffix
- (* systematically adds a _nnn suffix even if the original name
- ends with _mmm *)
+ (* systematically adds a _nnn suffix even if the original name
+ ends with _mmm *)
let has_generated_prefix n prefix =
let prefix_length = String.length prefix in
@@ -79,39 +79,39 @@ let has_generated_prefix n prefix =
end else n
in
String.length real_name >= prefix_length &&
- String.sub real_name 0 prefix_length = prefix
+ String.sub real_name 0 prefix_length = prefix
let generated_prefixes = [ "__anon"; "__constr_expr" ]
let is_generated_name n =
List.exists (has_generated_prefix n) generated_prefixes
-(* Strip the suffix. Return the prefix, the suffix (including the separator
- * but not the numeric value, possibly empty), and the
- * numeric value of the suffix (possibly -1 if missing) *)
-let splitNameForAlpha ~(lookupname: string) =
+(* Strip the suffix. Return the prefix, the suffix (including the separator
+ * but not the numeric value, possibly empty), and the
+ * numeric value of the suffix (possibly -1 if missing) *)
+let splitNameForAlpha ~(lookupname: string) =
let len = String.length lookupname in
- (* Search backward for the numeric suffix. Return the first digit of the
+ (* Search backward for the numeric suffix. Return the first digit of the
* suffix. Returns len if no numeric suffix *)
let rec skipSuffix seen_sep last_sep (i: int) =
if i = -1 then last_sep else
- let c = lookupname.[i] in
- (* we might start to use Str at some point. *)
- if (Char.compare '0' c <= 0 && Char.compare c '9' <= 0) then
- skipSuffix false last_sep (i - 1)
- else if c = alphaSeparator then
- if not seen_sep then
- (* check whether we are in the middle of a multi-suffix ident
- e.g. x_0_2, where the prefix would be x. *)
- skipSuffix true i (i-1)
- else (* we have something like x__0. Consider x_ as the prefix. *)
- i+1
- else (* we have something like x1234_0. Consider x1234 as the prefix *)
- last_sep
+ let c = lookupname.[i] in
+ (* we might start to use Str at some point. *)
+ if (Char.compare '0' c <= 0 && Char.compare c '9' <= 0) then
+ skipSuffix false last_sep (i - 1)
+ else if c = alphaSeparator then
+ if not seen_sep then
+ (* check whether we are in the middle of a multi-suffix ident
+ e.g. x_0_2, where the prefix would be x. *)
+ skipSuffix true i (i-1)
+ else (* we have something like x__0. Consider x_ as the prefix. *)
+ i+1
+ else (* we have something like x1234_0. Consider x1234 as the prefix *)
+ last_sep
in
(* we start as if the next char of the identifier was _, so that
x123_ is seen as a prefix.
- *)
+ *)
let startSuffix = skipSuffix true len (len - 1) in
if startSuffix >= len
then
@@ -129,11 +129,11 @@ let make_full_suffix infix n = infix ^ make_suffix n
elements of l are less than or equal to max.
returns the new suffix and a new bound to max in case the new suffix is
greater than max.
- *)
+*)
let find_unused_suffix min infix sibling l =
let rec aux v =
if List.exists (fun (n,_) -> Integer.equal n v) l
- || H.mem sibling (make_full_suffix infix v)
+ || H.mem sibling (make_full_suffix infix v)
then begin
Kernel.debug ~dkey:Kernel.dkey_alpha
"%s is already taken" (make_full_suffix infix v);
@@ -143,27 +143,27 @@ let find_unused_suffix min infix sibling l =
let get_suffix_idx rename_mode infix =
match rename_mode with
- | Add_new_suffix -> infix, Integer.minus_one
- | Incr_last_suffix when infix = "" -> infix, Integer.minus_one
- | Incr_last_suffix ->
- (* by construction there is at least one alphaSeparator in the infix *)
- let idx = String.rindex infix alphaSeparator in
- String.sub infix 0 idx,
- Integer.of_string
- (String.sub infix (idx + 1) (String.length infix - idx - 1))
+ | Add_new_suffix -> infix, Integer.minus_one
+ | Incr_last_suffix when infix = "" -> infix, Integer.minus_one
+ | Incr_last_suffix ->
+ (* by construction there is at least one alphaSeparator in the infix *)
+ let idx = String.rindex infix alphaSeparator in
+ String.sub infix 0 idx,
+ Integer.of_string
+ (String.sub infix (idx + 1) (String.length infix - idx - 1))
-(* Create a new name based on a given name. The new name is formed from a
- * prefix (obtained from the given name by stripping a suffix consisting of
- * the alphaSeparator followed by only digits), followed by alphaSeparator
- * and then by a positive integer suffix. The first argument is a table
- * mapping name prefixes to the largest suffix used so far for that
- * prefix. The largest suffix is one when only the version without suffix has
+(* Create a new name based on a given name. The new name is formed from a
+ * prefix (obtained from the given name by stripping a suffix consisting of
+ * the alphaSeparator followed by only digits), followed by alphaSeparator
+ * and then by a positive integer suffix. The first argument is a table
+ * mapping name prefixes to the largest suffix used so far for that
+ * prefix. The largest suffix is one when only the version without suffix has
* been used. *)
let alphaWorker ~(alphaTable: 'a alphaTable)
- ?undolist
- ~(lookupname: string) ~(data:'a)
- (make_new: bool) : string * 'a =
+ ?undolist
+ ~(lookupname: string) ~(data:'a)
+ (make_new: bool) : string * 'a =
let prefix, infix = splitNameForAlpha ~lookupname in
let rename_mode =
if is_generated_name prefix then Incr_last_suffix else Add_new_suffix
@@ -179,66 +179,66 @@ let alphaWorker ~(alphaTable: 'a alphaTable)
let min, suffixes = !rc in
(* We have seen this prefix *)
Kernel.debug ~dkey:Kernel.dkey_alpha "Old min %s. Old suffixes: @[%a@]"
- (Integer.to_string min)
+ (Integer.to_string min)
(Pretty_utils.pp_list
(fun fmt (s,_) -> Format.fprintf fmt "%s" (Integer.to_string s)))
suffixes;
(* Save the undo info *)
(match undolist with
- Some l -> l := AlphaChangedSuffix (rc, !rc) :: !l
- | _ -> ());
+ Some l -> l := AlphaChangedSuffix (rc, !rc) :: !l
+ | _ -> ());
let newname, newmin, (olddata: 'a), newsuffixes =
match
List.filter (fun (n, _) -> Integer.equal n curr_idx) suffixes
with
- | [] -> (* never seen this index before *)
- lookupname, min, data, (curr_idx, data) :: suffixes
- | [(_, l) ] ->
- (* We have seen this exact suffix before *)
- (* In Incr_last_suffix mode, we do not take curr_idx into account,
- but select the first available index available *)
- if make_new then begin
- let newmin =
- find_unused_suffix (Integer.succ min) infix infixes suffixes
- in
- let newsuffix = make_suffix newmin in
- let newinfix = make_full_suffix infix newmin in
- Kernel.(
- debug ~dkey:dkey_alpha "New suffix: %s" newsuffix);
- let base =
- if is_generated_name prefix then prefix else lookupname
- in
- H.add
- infixes newinfix
- (ref (Integer.minus_one, [(Integer.minus_one, data)]));
- (match undolist with
- | Some l -> l:= AlphaAddedSuffix (prefix,newsuffix)::!l
- | None -> ());
- base ^ newsuffix, newmin, l, (newmin, data) :: suffixes
- end else lookupname, min, data, suffixes
- | _ -> (Kernel.fatal "Cil.alphaWorker")
+ | [] -> (* never seen this index before *)
+ lookupname, min, data, (curr_idx, data) :: suffixes
+ | [(_, l) ] ->
+ (* We have seen this exact suffix before *)
+ (* In Incr_last_suffix mode, we do not take curr_idx into account,
+ but select the first available index available *)
+ if make_new then begin
+ let newmin =
+ find_unused_suffix (Integer.succ min) infix infixes suffixes
+ in
+ let newsuffix = make_suffix newmin in
+ let newinfix = make_full_suffix infix newmin in
+ Kernel.(
+ debug ~dkey:dkey_alpha "New suffix: %s" newsuffix);
+ let base =
+ if is_generated_name prefix then prefix else lookupname
+ in
+ H.add
+ infixes newinfix
+ (ref (Integer.minus_one, [(Integer.minus_one, data)]));
+ (match undolist with
+ | Some l -> l:= AlphaAddedSuffix (prefix,newsuffix)::!l
+ | None -> ());
+ base ^ newsuffix, newmin, l, (newmin, data) :: suffixes
+ end else lookupname, min, data, suffixes
+ | _ -> (Kernel.fatal "Cil.alphaWorker")
in
rc := (newmin, newsuffixes);
newname, olddata
with Not_found -> begin (* First variable with this prefix *)
- (match undolist with
- Some l -> l := AlphaAddedSuffix (prefix,infix) :: !l
- | _ -> ());
- let infixes =
- try H.find alphaTable prefix
- with Not_found ->
- let h = H.create 3 in H.add alphaTable prefix h; h
- in
- H.add infixes infix
- (ref (Integer.minus_one, [ (curr_idx, data) ]));
- Kernel.debug ~dkey:Kernel.dkey_alpha " First seen. ";
- lookupname, data (* Return the original name *)
- end
+ (match undolist with
+ Some l -> l := AlphaAddedSuffix (prefix,infix) :: !l
+ | _ -> ());
+ let infixes =
+ try H.find alphaTable prefix
+ with Not_found ->
+ let h = H.create 3 in H.add alphaTable prefix h; h
+ in
+ H.add infixes infix
+ (ref (Integer.minus_one, [ (curr_idx, data) ]));
+ Kernel.debug ~dkey:Kernel.dkey_alpha " First seen. ";
+ lookupname, data (* Return the original name *)
+ end
in
Kernel.debug ~dkey:Kernel.dkey_alpha "Res=: %s" newname;
newname, olddata
-
+
let newAlphaName ~alphaTable ?undolist ~lookupname ~data =
alphaWorker ~alphaTable ?undolist ~lookupname ~data true
@@ -249,11 +249,11 @@ let registerAlphaName ~alphaTable ?undolist ~lookupname ~data =
let getAlphaPrefix ~lookupname = splitNameForAlpha ~lookupname
(* Undoes the changes as specified by the undolist *)
-let undoAlphaChanges ~alphaTable ~undolist =
+let undoAlphaChanges ~alphaTable ~undolist =
List.iter
- (function
- AlphaChangedSuffix (where, old) ->
- where := old
+ (function
+ AlphaChangedSuffix (where, old) ->
+ where := old
| AlphaAddedSuffix (prefix, infix) ->
Kernel.debug ~dkey:Kernel.dkey_alpha_undo
"Removing %s%s from alpha table\n" prefix infix;
@@ -266,4 +266,3 @@ let undoAlphaChanges ~alphaTable ~undolist =
"prefix %s has no entry in the table. Inconsistent undo list"
prefix)
undolist
-
diff --git a/src/kernel_internals/typing/alpha.mli b/src/kernel_internals/typing/alpha.mli
index 852b6791ab4784f1b6f0fb05e8867759e8199015..9101266f4187f9bad0896d686939301ff27b8c3b 100644
--- a/src/kernel_internals/typing/alpha.mli
+++ b/src/kernel_internals/typing/alpha.mli
@@ -43,52 +43,52 @@
(** Alpha conversion. *)
-(** This is the type of the elements that are recorded by the alpha
- * conversion functions in order to be able to undo changes to the tables
- * they modify. Useful for implementing
+(** This is the type of the elements that are recorded by the alpha
+ * conversion functions in order to be able to undo changes to the tables
+ * they modify. Useful for implementing
* scoping *)
type 'a undoAlphaElement
-(** This is the type of the elements of the alpha renaming table. These
+(** This is the type of the elements of the alpha renaming table. These
* elements can carry some data associated with each occurrence of the name. *)
type 'a alphaTableData
(** type for alpha conversion table. We split the lookup in two to avoid
creating accidental collisions when converting x_0 into x_0_0 if the
original code contains both. *)
-type 'a alphaTable =
+type 'a alphaTable =
(string, (string, 'a alphaTableData ref) Hashtbl.t) Hashtbl.t
-(** Create a new name based on a given name. The new name is formed from a
- * prefix (obtained from the given name by stripping a suffix consisting of _
- * followed by only digits), followed by a special separator and then by a
- * positive integer suffix. The first argument is a table mapping name
- * prefixes to some data that specifies what suffixes have been used and how
- * to create the new one. This function updates the table with the new
- * largest suffix generated. The "undolist" argument, when present, will be
- * used by the function to record information that can be used by
- * {!Alpha.undoAlphaChanges} to undo those changes. Note that the undo
- * information will be in reverse order in which the action occurred. Returns
- * the new name and, if different from the lookupname, the location of the
- * previous occurrence. This function knows about the location implicitly
+(** Create a new name based on a given name. The new name is formed from a
+ * prefix (obtained from the given name by stripping a suffix consisting of _
+ * followed by only digits), followed by a special separator and then by a
+ * positive integer suffix. The first argument is a table mapping name
+ * prefixes to some data that specifies what suffixes have been used and how
+ * to create the new one. This function updates the table with the new
+ * largest suffix generated. The "undolist" argument, when present, will be
+ * used by the function to record information that can be used by
+ * {!Alpha.undoAlphaChanges} to undo those changes. Note that the undo
+ * information will be in reverse order in which the action occurred. Returns
+ * the new name and, if different from the lookupname, the location of the
+ * previous occurrence. This function knows about the location implicitly
* from the [(Cil.CurrentLoc.get ())]. *)
val newAlphaName: alphaTable: 'a alphaTable ->
- ?undolist: 'a undoAlphaElement list ref ->
- lookupname:string -> data:'a -> string * 'a
+ ?undolist: 'a undoAlphaElement list ref ->
+ lookupname:string -> data:'a -> string * 'a
-(** Register a name with an alpha conversion table to ensure that when later
+(** Register a name with an alpha conversion table to ensure that when later
* we call newAlphaName we do not end up generating this one *)
val registerAlphaName: alphaTable: 'a alphaTable ->
- ?undolist: 'a undoAlphaElement list ref ->
- lookupname:string -> data:'a -> unit
+ ?undolist: 'a undoAlphaElement list ref ->
+ lookupname:string -> data:'a -> unit
-(** Split the name in preparation for newAlphaName. Returns a pair
+(** Split the name in preparation for newAlphaName. Returns a pair
[(prefix, infix)] where [prefix] is the index in the outer table, while
infix is the index in the inner table.
*)
val getAlphaPrefix: lookupname:string -> string * string
(** Undo the changes to a table *)
-val undoAlphaChanges: alphaTable:'a alphaTable ->
- undolist:'a undoAlphaElement list -> unit
+val undoAlphaChanges: alphaTable:'a alphaTable ->
+ undolist:'a undoAlphaElement list -> unit