diff --git a/Makefile b/Makefile
index d434977cc7305f3d03a6a55f36e40ebabe4c9c77..c20cc4211159b2fee1d40043b7e9d1625cbfc63c 100644
--- a/Makefile
+++ b/Makefile
@@ -900,6 +900,7 @@ PLUGIN_CMO:= partitioning/split_strategy value_parameters \
engine/subdivided_evaluation engine/evaluation engine/abstractions \
engine/recursion engine/transfer_stmt engine/transfer_specification \
engine/partitioning_index engine/mem_exec \
+ partitioning/auto_loop_unroll \
engine/partition partitioning/partitioning_parameters \
engine/trace_partitioning \
engine/iterator \
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index 644e3bf20b5a617f34df40a686b12dadabab3bf4..eb378dc20bbd738c1af9512c6a722d57450098c7 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -164,6 +164,7 @@ let to_list (p : 'a partition) : 'a list =
type unroll_limit =
| ExpLimit of Cil_types.exp
| IntLimit of int
+ | AutoUnroll of Cil_types.stmt * int * int
type split_kind = Static | Dynamic
@@ -219,7 +220,11 @@ struct
let union (p1 : t) (p2 : t) : t =
p1 @ p2
- (* --- Evalution and split functions -------------------------------------- *)
+ (* --- Automatic loop unrolling ------------------------------------------- *)
+
+ module AutoLoopUnroll = Auto_loop_unroll.Make (Abstract)
+
+ (* --- Evaluation and split functions ------------------------------------- *)
(* Domains transfer functions. *)
module TF = Abstract.Dom.Transfer (Abstract.Eval.Valuation)
@@ -403,6 +408,14 @@ struct
let limit = try match limit_kind with
| ExpLimit exp -> eval_exp_to_int x exp
| IntLimit i -> i
+ | AutoUnroll (stmt, min_unroll, max_unroll) ->
+ match AutoLoopUnroll.compute ~max_unroll x stmt with
+ | None -> min_unroll
+ | Some i ->
+ Value_parameters.warning ~once:true ~current:true
+ ~wkey:Value_parameters.wkey_loop_unroll
+ "Automatic loop unrolling.";
+ i
with
| Operation_failed -> 0
in
diff --git a/src/plugins/value/engine/partition.mli b/src/plugins/value/engine/partition.mli
index 2a5177c756849b8abeb1bebb32e939066a11374f..cf1c7426b1d5a4dffcf9f10ce5b9278579ca45a9 100644
--- a/src/plugins/value/engine/partition.mli
+++ b/src/plugins/value/engine/partition.mli
@@ -76,12 +76,16 @@ type rationing
(** Creates a new rationing, that can be used successively on several flows. *)
val new_rationing: limit:int -> merge:bool -> rationing
-(** The unroll limit of a loop can be specified as an integer, or as a C
- expression, which is evaluated when entering the loop in each incoming
- state. The expression must always evaluate to a singleton integer. *)
+(** The unroll limit of a loop. *)
type unroll_limit =
| ExpLimit of Cil_types.exp
+ (** Value of the expression for each incoming state. The expression must
+ evaluate to a singleton integer in each state. *)
| IntLimit of int
+ (** Integer limit. *)
+ | AutoUnroll of Cil_types.stmt * int * int
+ (** [AutoUnroll(stmt, min, max)] requests to find a "good" unrolling limit
+ between [min] and [max] for the loop [stmt]. *)
(** Splits on an expression can be static or dynamic:
- static splits are processed once: the expression is only evaluated at the
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9620f6e21f7bd9d26cc01c79b9f8ebfb1e5355b6
--- /dev/null
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -0,0 +1,422 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Heuristic for automatic loop unrolling: when the number of iterations of a
+ loop can be bounded under a given limit, then unroll the loop.
+ The limit is defined by the option -eva-auto-loop-unroll. *)
+
+(* Gist of the heuristic:
+ - find a loop exit condition, in the form of a statement "if(cond) break;".
+ such that exactly one lvalue [lval] in the condition [cond] is modified
+ within the loop; all other lvalues must be constant in the loop.
+ - find a value [v_exit] such that [lval] ∈ [v_exit] ⇒ [cond] holds.
+ - evaluate [lval] to its initial value [v_init] in the loop entry state.
+ - compute an over-approximation of the increment [v_delta] of [lval] in one
+ iteration of the loop.
+
+ If [v_init] + k × [v_delta] ⊂ [v_exit], then the number of iterations
+ is bounded by the limit [k].
+
+ The heuristic is syntactic and limited to the current function: it does not
+ handle assignment through pointers or function calls.
+ Thus, the condition [cond] must only contains direct accesses to variables
+ whose address is never taken (they cannot be modified through pointers). If
+ the loop contains a function call, the condition [cond] must not contain any
+ global variable (as they may be modified in the function called).
+ A first analyze of the loop gathers all such variables modified within the
+ loop; all others are constant, and can be evaluated in the loop entry state.
+
+ When computing the increment [v_delta] of a lvalue [v] in the loop, the
+ heuristic searches assignments "v = v ± i;". Any other assignment of [v]
+ cancels the heuristic. *)
+
+open Cil_types
+
+(* Is a statement a loop exit condition? If so, returns the condition and
+ whether the condition must hold to exit the loop. Otherwise, returns None. *)
+let is_conditional_break stmt =
+ match stmt.skind with
+ | If (cond, {bstmts=[{skind=Break _}]}, _, _) -> Some (cond, true)
+ | If (cond, _, {bstmts=[{skind=Break _}]}, _) -> Some (cond, false)
+ | _ -> None
+
+(* Returns a loop exit condition, as the conditional expression and whether
+ the condition must be zero or non-zero to exit the loop. *)
+let find_loop_exit_condition loop =
+ let rec aux = function
+ | [] -> None
+ | stmt :: tl ->
+ match is_conditional_break stmt with
+ | Some _ as x -> x
+ | None -> aux tl
+ in
+ aux loop.bstmts
+
+(* Effects of a loop:
+ - set of varinfos that are directly modified within the loop. Pointer
+ accesses are ignored.
+ - does the loop contain a call? If so, any global variable may also be
+ modified in the loop. *)
+type loop_effect =
+ { written_vars: Cil_datatype.Varinfo.Set.t;
+ call: bool; }
+
+(* Visitor to compute the effects of a loop. *)
+let loop_effect_visitor = object (self)
+ inherit Visitor.frama_c_inplace
+
+ val mutable written_vars = Cil_datatype.Varinfo.Set.empty
+ val mutable call = false
+ val mutable assembly = false
+
+ (* Returns None if the loop contains assembly code. *)
+ method compute_effect block =
+ written_vars <- Cil_datatype.Varinfo.Set.empty;
+ call <- false;
+ assembly <- false;
+ ignore Visitor.(visitFramacBlock (self :> frama_c_inplace) block);
+ if assembly then None else Some { written_vars; call; }
+
+ method !vinst instr =
+ let () = match instr with
+ | Set ((Var varinfo, _), _, _)
+ | Call (Some (Var varinfo, _), _, _, _) ->
+ written_vars <- Cil_datatype.Varinfo.Set.add varinfo written_vars;
+ | _ -> ()
+ in
+ let () = match instr with
+ | Asm _ -> assembly <- true
+ | Call _ -> call <- true
+ | _ -> ()
+ in
+ Cil.SkipChildren
+end
+
+(* The status of a lvalue for the automatic loop unroll heuristic. *)
+type var_status =
+ | Constant (* The lvalue is constant within the loop. *)
+ | Candidate (* The lvalue is a good candidate for the heuristic:
+ integer type, access to a varinfo whose address is not taken,
+ modified within the loop but not in another function called
+ in the loop. *)
+ | Unsuitable (* Cannot be used for the heuristic. *)
+
+let is_integer lval = Cil.isIntegralType (Cil.typeOfLval lval)
+
+(* Computes the status of a lvalue for the heuristic, according to the
+ loop effects. *)
+let classify loop_effect lval =
+ let rec is_const_expr expr =
+ match expr.enode with
+ | Lval lval -> classify_lval lval = Constant
+ | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> is_const_expr e
+ | BinOp (_, e1, e2, _) -> is_const_expr e1 && is_const_expr e2
+ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
+ | AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> true
+ and classify_lval = function
+ | Var varinfo, offset ->
+ if varinfo.vaddrof
+ || (varinfo.vglob && loop_effect.call)
+ || not (is_const_offset offset)
+ then Unsuitable
+ else if Cil_datatype.Varinfo.Set.mem varinfo loop_effect.written_vars
+ then if is_integer lval then Candidate else Unsuitable
+ else Constant
+ | Mem _, _ -> Unsuitable (* Pointers are not supported by the heuristic. *)
+ and is_const_offset = function
+ | NoOffset -> true
+ | Field (_, offset) -> is_const_offset offset
+ | Index (e, offset) -> is_const_expr e && is_const_offset offset
+ in
+ classify_lval lval
+
+(* Returns the list of all lvalues appearing in an expression. *)
+let rec get_lvalues expr =
+ match expr.enode with
+ | Lval lval -> [ lval ]
+ | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> get_lvalues e
+ | BinOp (_op, e1, e2, _typ) -> get_lvalues e1 @ get_lvalues e2
+ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
+ | AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> []
+
+(* Finds the unique candidate lvalue for the automatic loop unrolling
+ heuristic in the expression [expr], if it exists. Returns None otherwise. *)
+let find_lonely_candidate loop_effect expr =
+ let lvalues = get_lvalues expr in
+ let rec aux acc list =
+ match list with
+ | [] -> acc
+ | lval :: tl ->
+ match classify loop_effect lval with
+ | Unsuitable -> None
+ | Constant -> aux acc tl
+ | Candidate -> if acc = None then aux (Some lval) tl else None
+ in
+ aux None lvalues
+
+(* Returns true if the instruction assigns [lval]. *)
+let is_safe_instruction lval = function
+ | Set (lv, _, _)
+ | Call (Some lv, _, _, _) -> not (Cil_datatype.LvalStructEq.equal lval lv)
+ | Call (None, _, _, _) | Local_init _ | Skip _ | Code_annot _ -> true
+ | Asm _ -> false
+
+(* Returns true if the statement may assign [lval] during an iteration of the
+ loop [loop]. [lval] is a candidate for the automatic loop unroll heuristic,
+ and thus is modified within the loop. *)
+let is_safe lval ~loop stmt =
+ (* The current block being checked for a goto statement. *)
+ let current_block = ref None in
+ let rec is_safe_stmt stmt =
+ match stmt.skind with
+ | Instr instr -> is_safe_instruction lval instr
+ | Return _ | Break _ | Continue _ -> true
+ | If (_, b_then, b_else, _) -> is_safe_block b_then && is_safe_block b_else
+ | Block b
+ | Switch (_, b, _, _)
+ | Loop (_, b, _, _, _) -> is_safe_block b
+ | UnspecifiedSequence list ->
+ List.for_all (fun (stmt, _, _, _, _) -> is_safe_stmt stmt) list
+ | Goto (dest, _) -> begin
+ let dest_blocks = Kernel_function.find_all_enclosing_blocks !dest in
+ (* If the goto leaves the loop, then it is safe. *)
+ if List.mem loop dest_blocks then true else
+ (* If the goto moves into the block currently being checked, then it
+ is safe if the block is safe (which we are currently checking). *)
+ match !current_block with
+ | Some current_block when List.mem current_block dest_blocks -> true
+ | _ ->
+ (* Otherwise, we need to check that the whole block englobing
+ both the source and the destination of the goto is safe. *)
+ let block = Kernel_function.common_block !dest stmt in
+ current_block := Some block;
+ (* If this block is the loop itself, then it is not safe, as [lval]
+ is modified within the loop. *)
+ not (block = loop) && is_safe_block block
+ end
+ | _ -> false
+ (* A block is safe if all its statements are safe. *)
+ and is_safe_block block = List.for_all is_safe_stmt block.bstmts in
+ is_safe_stmt stmt
+
+
+module Make (Abstract: Abstractions.Eva) = struct
+
+ open Eval
+ open Abstract
+ module Valuation = Abstract.Eval.Valuation
+ module Clear_Valuation = Clear_Valuation (Valuation)
+
+ let (>>) v f = match v with `Value v -> f v | _ -> None
+ let (>>=) v f = match v with Some v -> f v | None -> None
+
+ (* Reduces the condition "[condition] = [positive]" to a sufficient hypothesis
+ on the value of the expression [expr]: computes a value [v] such that
+ if the expression [expr] evaluates to [v], then [condition] = [positive].
+ [valuation] contains additional hypotheses, i.e. the value of some constant
+ lvalues of the [condition]. All computations must be done in the top state
+ and in the given valuation. *)
+ let reduce_to_expr valuation ~expr ~condition ~positive =
+ let state = Abstract.Dom.top in
+ (* Assumes that the [condition] is [positive]. *)
+ fst (Eval.reduce ~valuation state condition positive)
+ >> fun resulting_valuation ->
+ (* Finds the value of [expr] in the resulting valuation. *)
+ Valuation.find resulting_valuation expr >> fun record ->
+ record.value.v >> fun value ->
+ (* If the value of [expr] is top, no reduction has been performed. *)
+ if Val.(equal top value) then None
+ else
+ (* Otherwise, re-evaluate the condition with the hypothesis that [expr]
+ evaluates to [value]. If the condition is satisfied, then
+ [expr] ∈ [value] ⇒ [condition] = [positive]. *)
+ let valuation = Valuation.add valuation expr record in
+ fst (Eval.evaluate ~valuation ~reduction:false state condition)
+ >> fun (_valuation, v) ->
+ let satisfied =
+ if positive
+ then not Val.(is_included zero v)
+ else Val.(equal zero v)
+ in
+ if satisfied then Some value else None
+
+ (* Same as [reduce_to_expr] above, but builds the proper valuation from the
+ [state]. [state] is the entry state of the loop, and [expr] is the only
+ part of [condition] that is not constant within the loop. [state] can thus
+ be used to evaluate all other subparts of [condition], before computing
+ the value of [expr] that satisfies [condition]. *)
+ let reduce_to_lval_from_state state lval condition positive =
+ let expr = Cil.new_exp ~loc:condition.eloc (Lval lval) in
+ (* Evaluate the [condition] in the given [state]. *)
+ fst (Eval.evaluate state condition) >> fun (valuation, _v) ->
+ (* In the resulting valuation, replace the value of [expr] by [top_int]
+ and removes all expressions depending on [expr]. *)
+ Valuation.find valuation expr >> fun record ->
+ let value = { record.value with v = `Value Val.top_int } in
+ let record = { record with value } in
+ let valuation =
+ Clear_Valuation.clear_englobing_exprs
+ valuation ~expr:condition ~subexpr:expr
+ in
+ let valuation = Valuation.add valuation expr record in
+ reduce_to_expr valuation ~expr ~condition ~positive
+
+ (* Over-approximation of the increment of a lvalue in one loop iteration.*)
+ type delta =
+ { current: Val.t or_bottom; (* current delta being computed*)
+ final: Val.t or_bottom; (* final delta after a continue statement. *)
+ }
+
+ let join_delta d1 d2 =
+ { current = Bottom.join Val.join d1.current d2.current;
+ final = Bottom.join Val.join d1.final d2.final; }
+
+ let final_delta delta = Bottom.join Val.join delta.current delta.final
+
+ (* Raised when no increment can be computed for the given lvalue in one
+ loop iteration. *)
+ exception NoIncrement
+
+ (* Adds or subtracts the integer value of [expr] to the current delta
+ [delta.current], according to [binop] which can be PlusA or MinusA.
+ Raises NoIncrement if [expr] is not a constant integer expression. *)
+ let add_to_delta binop delta expr =
+ let typ = Cil.typeOf expr in
+ match Cil.constFoldToInt expr with
+ | None -> raise NoIncrement
+ | Some i ->
+ let value = Val.inject_int typ i in
+ let current = match delta.current with
+ | `Bottom -> `Value value
+ | `Value v -> Val.forward_binop typ binop v value
+ in
+ { delta with current }
+
+ (* Adds to [delta] the increment from the assignement of [lval] to the value
+ of [expr]. Raises NoIncrement if this is not an increment of [lval]. *)
+ let rec delta_assign lval delta expr =
+ (* Is the expression [e] equal to the lvalue [lval] (modulo cast)? *)
+ let rec is_lval e = match e.enode with
+ | Lval lv -> Cil_datatype.LvalStructEq.equal lval lv
+ | CastE (typ, e) -> Cil.isIntegralType typ && is_lval e
+ | Info (e, _) -> is_lval e
+ | _ -> false
+ in
+ match expr.enode with
+ | BinOp ((PlusA | MinusA) as binop, e1, e2, _) ->
+ if is_lval e1
+ then add_to_delta binop delta e2
+ else if is_lval e2 && binop = PlusA
+ then add_to_delta binop delta e1
+ else raise NoIncrement
+ | CastE (typ, e) when Cil.isIntegralType typ -> delta_assign lval delta e
+ | Info (e, _) -> delta_assign lval delta e
+ | _ -> raise NoIncrement
+
+ let delta_instruction lval delta = function
+ | Set (lv, expr, _loc) ->
+ if Cil_datatype.LvalStructEq.equal lval lv
+ then delta_assign lval delta expr
+ else delta
+ | Call (Some lv, _, _, _) ->
+ if Cil_datatype.LvalStructEq.equal lval lv
+ then raise NoIncrement (* No increment can be computed for a call. *)
+ else delta
+ | Call (None, _, _, _) | Local_init _ | Skip _ | Code_annot _ -> delta
+ | Asm _ -> raise NoIncrement
+
+ (* Computes an over-approximation of the increment of [lval] in the block
+ [loop]. Only syntactic assignments of [lval] are considered, so [lval]
+ should be a direct access to a variable whose address is not taken,
+ and which should not be global if the loop contains function calls.
+ Returns None if no increment can be computed. *)
+ let compute_delta lval loop =
+ let rec delta_stmt acc stmt =
+ match stmt.skind with
+ | Instr instr -> delta_instruction lval acc instr
+ | Break _ ->
+ (* No increment, as the statement leaves the loop. *)
+ { current = `Bottom; final = `Bottom }
+ | Continue _ ->
+ (* The current increment becomes the final increment. *)
+ { current = `Bottom; final = final_delta acc }
+ | If (_e, b1, b2, _loc) ->
+ join_delta (delta_block acc b1) (delta_block acc b2)
+ | Block b -> delta_block acc b
+ | _ ->
+ (* For other statements, we only check that they do not modify [lval]. *)
+ if is_safe lval ~loop stmt then acc else raise NoIncrement
+ and delta_block acc block =
+ List.fold_left delta_stmt acc block.bstmts
+ in
+ try
+ let zero_delta = { current = `Value Val.zero; final = `Bottom; } in
+ let delta = delta_block zero_delta loop in
+ final_delta delta >> fun d -> Some d
+ with NoIncrement -> None
+
+ (* Evaluates the lvalue [lval] in the state [state]. Returns None if the value
+ may be undeterminate. *)
+ let evaluate_lvalue state lval =
+ fst (Eval.copy_lvalue state lval) >> fun (_valuation, flagged_value) ->
+ if not flagged_value.initialized || flagged_value.escaping
+ then None
+ else flagged_value.v >> fun v -> Some v
+
+ (* Is the number of iterations of a loop bounded by [limit]?
+ [state] is the loop entry state, and [loop_block] the block of the loop. *)
+ let is_bounded_loop state limit loop_block =
+ (* Computes the effect of the loop. Stops if it contains assembly code. *)
+ loop_effect_visitor#compute_effect loop_block >>= fun loop_effect ->
+ (* Finds the first loop exit condition, or stops. *)
+ find_loop_exit_condition loop_block >>= fun (condition, positive) ->
+ (* Finds the unique integer lvalue modified within the loop in [condition].
+ Stops if it does not exist is not a good candidate for the heuristic. *)
+ find_lonely_candidate loop_effect condition >>= fun lval ->
+ (* Reduce [condition] to a sufficient hypothesis over the [lval] value:
+ if [lval] ∈ [v_exit] then [condition = positive]. *)
+ reduce_to_lval_from_state state lval condition positive >>= fun v_exit ->
+ (* Evaluates the initial value [v_init] of [lval] in the loop entry state. *)
+ evaluate_lvalue state lval >>= fun v_init ->
+ (* Computes an over-approximation [v_delta] of the increment of [lval]
+ in one iteration of the loop. *)
+ compute_delta lval loop_block >>= fun v_delta ->
+ let typ = Cil.typeOfLval lval in
+ let limit = Val.inject_int typ (Integer.of_int limit) in
+ (* Checks whether [v_init] + [limit] × [v_delta] ⊂ [v_exit]. *)
+ let binop op v1 v2 = Bottom.non_bottom (Val.forward_binop typ op v1 v2) in
+ let value = binop PlusA v_init (binop Mult limit v_delta) in
+ Some (Val.is_included value v_exit)
+
+ (* Computes an automatic loop unrolling for statement [stmt] in state [state],
+ with a maximum limit. Returns None for no automatic loop unrolling. *)
+ let compute ~max_unroll state stmt =
+ try
+ let kf = Kernel_function.find_englobing_kf stmt in
+ let loop_stmt = Kernel_function.find_enclosing_loop kf stmt in
+ match loop_stmt.skind with
+ | Loop (_code_annot, block, _loc, _, _) ->
+ is_bounded_loop state max_unroll block >>= fun bounded ->
+ if bounded then Some max_unroll else None
+ | _ -> None
+ with Not_found -> None
+end
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.mli b/src/plugins/value/partitioning/auto_loop_unroll.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e16a7ec2e1d1f7e3567de026e8d35441c9e1cd75
--- /dev/null
+++ b/src/plugins/value/partitioning/auto_loop_unroll.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Heuristic for automatic loop unrolling. *)
+
+module Make (Abstract: Abstractions.Eva) : sig
+
+ val compute:
+ max_unroll:int -> Abstract.Dom.t -> Cil_types.stmt -> int option
+
+end
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index b480f4e425da2b3ce6f1dd62384c0ffd326a1151..33ad321a5cba2cdbbf4c053b7f77fb153a91656b 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -58,7 +58,7 @@ struct
!Db.Properties.Interp.term_to_exp ~result:None term
let min_loop_unroll = MinLoopUnroll.get ()
-
+ let auto_loop_unroll = AutoLoopUnroll.get ()
let default_loop_unroll = DefaultLoopUnroll.get ()
let warn_no_loop_unroll stmt =
@@ -76,7 +76,11 @@ struct
"%s loop without unroll annotation" loop_kind
let unroll stmt =
- let default = Partition.IntLimit min_loop_unroll in
+ let default =
+ if auto_loop_unroll > min_loop_unroll
+ then Partition.AutoUnroll (stmt, min_loop_unroll, auto_loop_unroll)
+ else Partition.IntLimit min_loop_unroll
+ in
match get_unroll_annot stmt with
| [] -> warn_no_loop_unroll stmt; default
| [None] -> Partition.IntLimit default_loop_unroll
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 0f972433fe475cecf2c6f1a3981bafea11ed233f..cd94d41a2ba0eb7db47daf8cc7d43ed7f61d92df 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -812,6 +812,20 @@ module MinLoopUnroll =
let () = add_precision_dep MinLoopUnroll.parameter
let () = MinLoopUnroll.set_range 0 max_int
+let () = Parameter_customize.set_group precision_tuning
+module AutoLoopUnroll =
+ Int
+ (struct
+ let option_name = "-eva-auto-loop-unroll"
+ let arg_name = "n"
+ let default = 128
+ let help = "limit of the automatic loop unrolling: all loops whose \
+ number of iterations can be easily bounded by <n> \
+ are completely unrolled."
+ end)
+let () = add_precision_dep AutoLoopUnroll.parameter
+let () = AutoLoopUnroll.set_range 0 max_int
+
let () = Parameter_customize.set_group precision_tuning
module DefaultLoopUnroll =
Int
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8cda781691b11799c8f0277f35bab8803cc53206..7ead8310a01f463bd9cd8f75d995a2ecce1af21a 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -93,6 +93,7 @@ module SlevelFunction:
module SlevelMergeAfterLoop: Parameter_sig.Kernel_function_set
module MinLoopUnroll : Parameter_sig.Int
+module AutoLoopUnroll : Parameter_sig.Int
module DefaultLoopUnroll : Parameter_sig.Int
module HistoryPartitioning : Parameter_sig.Int
module ValuePartitioning : Parameter_sig.String_set