diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index a317fca1878143ba241ca512e61dfed56eb30e47..498e4fdd241f24faf716fc5bc69c668705dd3e6a 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -571,6 +571,8 @@ module Eva_annotations: sig
type unroll_annotation =
| UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
| UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
+ | UnrollAuto of int (** Use the automatic loop unrolling with the given limit,
+ as if -eva-auto-loop-unroll N was locally set. *)
type split_kind = Static | Dynamic
diff --git a/src/plugins/eva/partitioning/partitioning_parameters.ml b/src/plugins/eva/partitioning/partitioning_parameters.ml
index d331531446bf78c9b260930d0302f1c3d0459528..9221c06ac9091004ba796f83ac283f9ae83efe4e 100644
--- a/src/plugins/eva/partitioning/partitioning_parameters.ml
+++ b/src/plugins/eva/partitioning/partitioning_parameters.ml
@@ -74,14 +74,16 @@ struct
"%s loop without unroll annotation" loop_kind
let unroll stmt =
- let default =
- if auto_loop_unroll > min_loop_unroll
- then Partition.AutoUnroll (stmt, min_loop_unroll, auto_loop_unroll)
+ let automatic_unrolling i =
+ if i > min_loop_unroll
+ then Partition.AutoUnroll (stmt, min_loop_unroll, i)
else Partition.IntLimit min_loop_unroll
in
+ let default = automatic_unrolling auto_loop_unroll in
match get_unroll_annot stmt with
| [] -> warn_no_loop_unroll stmt; default
| [UnrollFull] -> Partition.IntLimit default_loop_unroll
+ | [UnrollAuto i] -> automatic_unrolling i
| [UnrollAmount t] -> begin
(* Inlines the value of const variables in [t]. *)
let global_init vi =
@@ -98,8 +100,8 @@ struct
warn "invalid loop unrolling parameter; ignoring";
default
end
- | _ ->
- warn "invalid unroll annotation; ignoring";
+ | _ :: _ :: _ ->
+ warn "more than one loop unroll annotation; ignoring";
default
let history_size = HistoryPartitioning.get ()
diff --git a/src/plugins/eva/utils/eva_annotations.ml b/src/plugins/eva/utils/eva_annotations.ml
index d00ff4fd2825b1ac40b9811e2036ec2ff9b84a25..334d7565a90df0eae97eab6ca588105511a4900b 100644
--- a/src/plugins/eva/utils/eva_annotations.ml
+++ b/src/plugins/eva/utils/eva_annotations.ml
@@ -32,6 +32,7 @@ type slevel_annotation =
type unroll_annotation =
| UnrollAmount of Cil_types.term
| UnrollFull
+ | UnrollAuto of int
type split_kind = Static | Dynamic
type split_term =
@@ -180,20 +181,35 @@ module Unroll = Register (struct
let open Logic_typing in
UnrollAmount
(typing_context.type_term typing_context typing_context.pre_state t)
+ | [{lexpr_node = PLvar "auto"};
+ {lexpr_node = PLconstant (IntConstant i)}] ->
+ let i = match int_of_string i with
+ | i when i >= 0 -> i
+ | _i -> raise Parse_error
+ | exception Failure _ -> raise Parse_error
+ in
+ UnrollAuto i
| _ -> raise Parse_error
let export = function
| UnrollFull -> Ext_terms []
| UnrollAmount t -> Ext_terms [t]
+ | UnrollAuto i ->
+ Ext_terms [Logic_const.tstring "auto"; Logic_const.tinteger i]
let import = function
| Ext_terms [] -> UnrollFull
| Ext_terms [t] -> UnrollAmount t
+ | Ext_terms [
+ {term_node = TConst (LStr "auto")};
+ {term_node = TConst (Integer (i, _))}] ->
+ UnrollAuto (Integer.to_int_exn i)
| _ -> assert false
let print fmt = function
| UnrollFull -> ()
| UnrollAmount t -> Printer.pp_term fmt t
+ | UnrollAuto i -> Format.fprintf fmt "auto, %d" i
end)
module SplitTermAnnotation =
diff --git a/src/plugins/eva/utils/eva_annotations.mli b/src/plugins/eva/utils/eva_annotations.mli
index a56ce470ae9125b8bf154b00c7db743e1dfe60c7..8cd2ed06adf22729295d0828b8c58e7f33392767 100644
--- a/src/plugins/eva/utils/eva_annotations.mli
+++ b/src/plugins/eva/utils/eva_annotations.mli
@@ -43,6 +43,8 @@ type slevel_annotation =
type unroll_annotation =
| UnrollAmount of Cil_types.term (** Unroll the n first iterations. *)
| UnrollFull (** Unroll amount defined by -eva-default-loop-unroll. *)
+ | UnrollAuto of int (** Use the automatic loop unrolling with the given limit,
+ as if -eva-auto-loop-unroll N was locally set. *)
type split_kind = Static | Dynamic
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index ea9768af17d7484dcc0269ee930d6996a11dbb2f..3294c2b093f9bf1a6c502c10bd189bd06929b7cd 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function test_slevel <- main.
- Called from partitioning-annots.c:278.
+ Called from partitioning-annots.c:289.
[eva] partitioning-annots.c:243: starting to merge loop iterations
[eva] partitioning-annots.c:248: starting to merge loop iterations
[eva] Recording results for test_slevel
[eva] Done for function test_slevel
[eva] computing for function test_unroll <- main.
- Called from partitioning-annots.c:279.
+ Called from partitioning-annots.c:290.
[eva:loop-unroll:partial] partitioning-annots.c:26: loop not completely unrolled
[eva] partitioning-annots.c:26: starting to merge loop iterations
[eva:loop-unroll:partial] partitioning-annots.c:34: loop not completely unrolled
@@ -25,7 +25,7 @@
[eva] Recording results for test_unroll
[eva] Done for function test_unroll
[eva] computing for function test_split <- main.
- Called from partitioning-annots.c:280.
+ Called from partitioning-annots.c:291.
[eva] computing for function Frama_C_interval <- test_split <- main.
Called from partitioning-annots.c:73.
[eva] using specification for function Frama_C_interval
@@ -65,7 +65,7 @@
[eva] Recording results for test_split
[eva] Done for function test_split
[eva] computing for function test_dynamic_split <- main.
- Called from partitioning-annots.c:281.
+ Called from partitioning-annots.c:292.
[eva] partitioning-annots.c:95: Warning:
this partitioning parameter cannot be evaluated safely on all states
[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
@@ -90,12 +90,12 @@
[eva] Recording results for test_dynamic_split
[eva] Done for function test_dynamic_split
[eva] computing for function test_dynamic_split_predicate <- main.
- Called from partitioning-annots.c:282.
+ Called from partitioning-annots.c:293.
[eva] partitioning-annots.c:124: starting to merge loop iterations
[eva] Recording results for test_dynamic_split_predicate
[eva] Done for function test_dynamic_split_predicate
[eva] computing for function test_splits_post_call <- main.
- Called from partitioning-annots.c:283.
+ Called from partitioning-annots.c:294.
[eva] computing for function Frama_C_interval <- test_splits_post_call <- main.
Called from partitioning-annots.c:205.
[eva] partitioning-annots.c:205:
@@ -119,6 +119,12 @@
[eva] partitioning-annots.c:217: Frama_C_show_each_body: {-1}, [-1000..1000]
[eva] Recording results for test_splits_post_call
[eva] Done for function test_splits_post_call
+[eva] computing for function test_auto_limit <- main.
+ Called from partitioning-annots.c:295.
+[eva:loop-unroll:auto] partitioning-annots.c:280: Automatic loop unrolling.
+[eva] partitioning-annots.c:284: starting to merge loop iterations
+[eva] Recording results for test_auto_limit
+[eva] Done for function test_auto_limit
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
@@ -128,6 +134,8 @@
state ∈ {-1; 0; 1}
y ∈ [-1000..1000] or UNINITIALIZED
__retres ∈ [-510..510]
+[eva:final-states] Values at end of function test_auto_limit:
+
[eva:final-states] Values at end of function test_dynamic_split:
Frama_C_entropy_source ∈ [--..--]
a ∈ {0}
@@ -185,6 +193,8 @@
k ∈ {0; 1}
[from] Computing for function body
[from] Done for function body
+[from] Computing for function test_auto_limit
+[from] Done for function test_auto_limit
[from] Computing for function test_dynamic_split
[from] Computing for function Frama_C_interval <-test_dynamic_split
[from] Done for function Frama_C_interval
@@ -214,6 +224,8 @@
[from] Function spec:
x FROM i
\result FROM i
+[from] Function test_auto_limit:
+ NO EFFECTS
[from] Function test_dynamic_split:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
[from] Function test_dynamic_split_predicate:
@@ -235,6 +247,10 @@
i2; absolute; tmp; state; y; __retres
[inout] Inputs for function body:
nondet
+[inout] Out (internal) for function test_auto_limit:
+ i; i_0
+[inout] Inputs for function test_auto_limit:
+ \nothing
[inout] Out (internal) for function test_dynamic_split:
Frama_C_entropy_source; a; b
[inout] Inputs for function test_dynamic_split:
diff --git a/tests/value/oracle_apron/partitioning-annots.0.res.oracle b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
index 68d268103b83832bb45759df2b7108b8ad474e1e..4e3b70b39201f9d1fe5f8186bb1082350e7e6481 100644
--- a/tests/value/oracle_apron/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
@@ -10,7 +10,7 @@
> Called from partitioning-annots.c:212.
> [eva] Recording results for body
> [eva] Done for function body
-136,137c142,143
+144,145c150,151
< x ∈ [0..44]
< y ∈ [0..44]
---
diff --git a/tests/value/oracle_octagon/partitioning-annots.0.res.oracle b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
index 141d3a1f322385d29fea8cd73951c79d349d8440..d2a1e9742d6130d3fdb3e0af17461453825fcd68 100644
--- a/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
@@ -1,4 +1,4 @@
-136,137c136,137
+144,145c144,145
< x ∈ [0..44]
< y ∈ [0..44]
---
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index 6323f1df659d5f8bdc4864ea3df9fd88baaf82b2..169ca8b57aeb4982051cb5a8d4c896487fce059e 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -273,6 +273,17 @@ void test_slevel()
}
}
+void test_auto_limit()
+{
+ // This loop should be unrolled
+ //@ loop unroll auto, 30;
+ for (int i = 0; i < 20; i++) {}
+
+ // This loop should not be unrolled
+ //@ loop unroll auto, 5;
+ for (int i = 0; i < 20; i++) {}
+}
+
void main(void)
{
test_slevel();
@@ -281,4 +292,5 @@ void main(void)
test_dynamic_split();
test_dynamic_split_predicate();
test_splits_post_call();
+ test_auto_limit();
}