diff --git a/Makefile b/Makefile
index dd8b0234365cedef0c3d91c5f996c5e09fd151ae..d8e4d6405e58be280bce04571ebebad065f92984 100644
--- a/Makefile
+++ b/Makefile
@@ -860,9 +860,10 @@ endif
# General rules for ordering files within PLUGIN_CMO:
# - try to keep the legacy Value before Eva
PLUGIN_CMO:= partitioning/split_strategy value_parameters \
- utils/value_perf utils/value_util utils/red_statuses \
+ utils/value_perf utils/eva_annotations \
+ utils/value_util utils/red_statuses \
utils/mark_noresults \
- utils/widen_hints_ext utils/widen utils/partitioning_annots \
+ utils/widen_hints_ext utils/widen \
partitioning/split_return \
partitioning/per_stmt_slevel \
utils/library_functions \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index ad7a910447dba8edf011c15b02746bd9e3a48721..3e89f12518e8ee6a37d47076c045a8dd2c137848 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1328,8 +1328,8 @@ src/plugins/value/utils/red_statuses.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/library_functions.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/library_functions.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/mark_noresults.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/partitioning_annots.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/partitioning_annots.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/state_import.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/state_import.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 699f57b6e2443d8cbf912d37c306f30ddd3df2ba..c9ecc4766a4be390c9a5f677e1cc1e7388398b7d 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -196,20 +196,21 @@ module type S = sig
and type origin = origin
and type loc = loc
val evaluate :
- ?valuation:Valuation.t -> ?reduction:bool ->
+ ?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int ->
state -> exp -> (Valuation.t * value) evaluated
val copy_lvalue :
- ?valuation:Valuation.t ->
+ ?valuation:Valuation.t -> ?subdivnb:int ->
state -> lval -> (Valuation.t * value flagged_value) evaluated
val lvaluate :
- ?valuation:Valuation.t -> for_writing:bool ->
+ ?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool ->
state -> lval -> (Valuation.t * loc * typ) evaluated
val reduce:
?valuation:Valuation.t -> state -> exp -> bool -> Valuation.t evaluated
val assume:
?valuation:Valuation.t -> state -> exp -> value -> Valuation.t or_bottom
val eval_function_exp:
- exp -> ?args:exp list -> state -> (Kernel_function.t * Valuation.t) list evaluated
+ ?subdivnb:int -> exp -> ?args:exp list -> state ->
+ (Kernel_function.t * Valuation.t) list evaluated
val interpret_truth:
alarm:(unit -> Alarms.t) -> 'a -> 'a Abstract_value.truth -> 'a evaluated
end
@@ -741,21 +742,35 @@ module Make
Forward Evaluation
------------------------------------------------------------------------ *)
- (* Makes the oracle for the domain queries, called by the forward evaluation.
- Defined below, after applying the subdivided_evaluation to the forward
- evaluation function. *)
- let make_oracle = ref (fun _ _ _ -> `Value Value.top, Alarmset.all)
+ (* The forward evaluation context: arguments that must be passed through
+ the mutually recursive evaluation functions without being modified. *)
+ type context =
+ { (* The abstract domain state in which the evaluation takes place. *)
+ state: Domain.t;
+ (* Maximum number of subdivisions. See {!Subdivided_evaluation} for
+ more details. *)
+ subdivision: int;
+ (* The remaining fuel: maximum number of nested oracle uses, decremented
+ at each call to the oracle. *)
+ remaining_fuel: int;
+ (* The oracle which can be used by abstract domains to get a value for
+ some expressions. *)
+ oracle: context -> exp -> Value.t evaluated;
+ }
+
+ (* Builds the oracle from the context. *)
+ let make_oracle context = context.oracle context
(* Returns the cached value and alarms for the evaluation if it exists;
call [coop_forward_eval] and caches its result otherwise.
Also returns a boolean indicating whether the expression is volatile. *)
- let rec root_forward_eval fuel state expr =
+ let rec root_forward_eval context expr =
(* Search in the cache for the result of a previous computation. *)
try
let record, report = Cache.find' !cache expr in
(* If the record was computed with more fuel than [fuel], return it. *)
if report.fuel = Loop then fuel_consumed := true;
- if less_fuel_than fuel report.fuel
+ if less_fuel_than context.remaining_fuel report.fuel
then (record.value.v >>-: fun v -> v, report.volatile), record.val_alarms
else raise Not_found
(* If no result found, evaluate the expression. *)
@@ -766,7 +781,7 @@ module Make
(* Fill the cache to avoid loops in the use of the oracle. *)
cache := Cache.add' !cache expr (top_record, dummy_report);
(* Evaluation of [expr]. *)
- let result, alarms = coop_forward_eval fuel state expr in
+ let result, alarms = coop_forward_eval context expr in
let value =
result >>- fun (record, reduction, volatile) ->
(* Put the alarms in the record. *)
@@ -774,6 +789,7 @@ module Make
(* Inter-reduction of the value (in case of a reduced product). *)
let record = reduce_value record in
(* Cache the computed result with an appropriate report. *)
+ let fuel = context.remaining_fuel in
let fuel = if !fuel_consumed then Finite fuel else Infty in
let report = {fuel; reduction; volatile} in
cache := Cache.add' !cache expr (record, report);
@@ -783,7 +799,7 @@ module Make
fuel_consumed := previous_fuel_consumed || !fuel_consumed;
value, alarms
- and forward_eval fuel state expr = root_forward_eval fuel state expr >>=: fst
+ and forward_eval context expr = root_forward_eval context expr >>=: fst
(* The functions below returns, along with the computed value (when it is not
bottom):
@@ -794,12 +810,13 @@ module Make
(* Asks the abstract domain for abstractions (value and alarms) of [expr],
and performs the narrowing with the abstractions computed by
[internal_forward_eval]. *)
- and coop_forward_eval fuel state expr =
+ and coop_forward_eval context expr =
match expr.enode with
- | Lval lval -> eval_lval fuel state lval
+ | Lval lval -> eval_lval context lval
| BinOp _ | UnOp _ | CastE _ -> begin
- let intern_value, alarms = internal_forward_eval fuel state expr in
- let oracle = !make_oracle fuel state in
+ let intern_value, alarms = internal_forward_eval context expr in
+ let state = context.state in
+ let oracle = make_oracle context in
let domain_value, alarms' = Domain.extract_expr oracle state expr in
(* Intersection of alarms, as each sets of alarms are correct
and "complete" for the evaluation of [expr]. *)
@@ -828,7 +845,7 @@ module Make
v, alarms
end
| _ ->
- internal_forward_eval fuel state expr
+ internal_forward_eval context expr
>>=: fun (value, reduction, volatile) ->
let value = define_value value
and origin = None
@@ -837,39 +854,39 @@ module Make
reduction, volatile
(* Recursive descent in the sub-expressions. *)
- and internal_forward_eval fuel state expr =
+ and internal_forward_eval context expr =
let compute_reduction (v, a) volatile =
(v, a) >>=: fun v ->
let reduction = if Alarmset.is_empty a then Neither else Forward in
v, reduction, volatile
in
match expr.enode with
- | Info (e, _) -> internal_forward_eval fuel state e
- | Const constant -> internal_forward_eval_constant fuel state expr constant
+ | Info (e, _) -> internal_forward_eval context e
+ | Const constant -> internal_forward_eval_constant context expr constant
| Lval _lval -> assert false
| AddrOf v | StartOf v ->
- lval_to_loc fuel ~for_writing:false ~reduction:false state v
+ lval_to_loc context ~for_writing:false ~reduction:false v
>>=: fun (loc, _, _) ->
Loc.to_value loc, Neither, false
| UnOp (op, e, typ) ->
- root_forward_eval fuel state e >>= fun (v, volatile) ->
+ root_forward_eval context e >>= fun (v, volatile) ->
forward_unop op (e, v) >>= fun v ->
let may_overflow = op = Neg in
let v = handle_overflow ~may_overflow expr typ v in
compute_reduction v volatile
| BinOp (op, e1, e2, typ) ->
- root_forward_eval fuel state e1 >>= fun (v1, volatile1) ->
- root_forward_eval fuel state e2 >>= fun (v2, volatile2) ->
+ root_forward_eval context e1 >>= fun (v1, volatile1) ->
+ root_forward_eval context e2 >>= fun (v2, volatile2) ->
forward_binop typ (e1, v1) op (e2, v2) >>= fun v ->
let may_overflow = may_overflow op in
let v = handle_overflow ~may_overflow expr typ v in
compute_reduction v (volatile1 || volatile2)
| CastE (dst, e) ->
- root_forward_eval fuel state e >>= fun (value, volatile) ->
+ root_forward_eval context e >>= fun (value, volatile) ->
let v = forward_cast ~dst e value in
let v = match Cil.unrollType dst with
| TFloat (fkind, _) -> v >>= remove_special_float expr fkind
@@ -882,9 +899,9 @@ module Make
| Some v -> return (Value.inject_int (Cil.typeOf expr) v, Neither, false)
| _ -> return (Value.top_int, Neither, false)
- and internal_forward_eval_constant fuel state expr constant =
+ and internal_forward_eval_constant context expr constant =
let eval = match constant with
- | CEnum {eival = e} -> forward_eval fuel state e
+ | CEnum {eival = e} -> forward_eval context e
| CReal (_f, fkind, _fstring) ->
let value = Value.constant expr constant in
remove_special_float expr fkind value
@@ -907,13 +924,14 @@ module Make
If the location is not bottom, the function also returns the typ of the
lvalue, and a boolean indicating that the lvalue contains a sub-expression
with volatile qualifier (in its host or offset). *)
- and lval_to_loc fuel ~for_writing ~reduction state lval =
+ and lval_to_loc context ~for_writing ~reduction lval =
let compute () =
let res, alarms =
- reduced_lval_to_loc fuel ~for_writing ~reduction state lval
+ reduced_lval_to_loc context ~for_writing ~reduction lval
in
let res =
res >>-: fun (loc, typ_offs, red, volatile) ->
+ let fuel = context.remaining_fuel in
let record = { loc; typ = typ_offs; loc_alarms = alarms }
and report = { fuel = Finite fuel; reduction = red; volatile }
and loc_report = { for_writing; with_reduction = reduction } in
@@ -926,15 +944,15 @@ module Make
| `Value (record, (report, loc_report)) ->
if
already_precise_loc_report ~for_writing ~reduction loc_report
- && less_fuel_than fuel report.fuel
+ && less_fuel_than context.remaining_fuel report.fuel
then `Value (record.loc, record.typ, report.volatile), record.loc_alarms
else compute ()
| `Top -> compute ()
(* If [reduction] is false, don't reduce the location and the offset by their
valid parts, and don't emit alarms about their validity. *)
- and reduced_lval_to_loc fuel ~for_writing ~reduction state lval =
- internal_lval_to_loc fuel ~for_writing ~reduction state lval
+ and reduced_lval_to_loc context ~for_writing ~reduction lval =
+ internal_lval_to_loc context ~for_writing ~reduction lval
>>= fun (loc, typ, volatile) ->
if not reduction
then `Value (loc, typ, Neither, volatile), Alarmset.none
@@ -954,13 +972,13 @@ module Make
(* Internal evaluation of a lvalue to an abstract location.
Combination of the evaluation of the right part of an lval (an host) with
an offset, to obtain a location *)
- and internal_lval_to_loc fuel ~for_writing ~reduction state lval =
+ and internal_lval_to_loc context ~for_writing ~reduction lval =
let host, offset = lval in
let typ = match host with
| Var host -> host.vtype
| Mem x -> Cil.typeOf_pointed (Cil.typeOf x)
in
- eval_offset fuel ~reduce_valid_index:reduction typ state offset
+ eval_offset context ~reduce_valid_index:reduction typ offset
>>= fun (offs, typ_offs, offset_volatile) ->
if for_writing && Value_util.is_const_write_invalid typ_offs
then
@@ -968,33 +986,33 @@ module Make
Alarmset.singleton ~status:Alarmset.False
(Alarms.Memory_access (lval, Alarms.For_writing))
else
- eval_host fuel state typ_offs offs host >>=: fun (loc, host_volatile) ->
+ eval_host context typ_offs offs host >>=: fun (loc, host_volatile) ->
loc, typ_offs, offset_volatile || host_volatile
(* Host evaluation. Also returns a boolean which is true if the host
contains a volatile sub-expression. *)
- and eval_host fuel state typ_offset offs = function
+ and eval_host context typ_offset offs = function
| Var host ->
(Loc.forward_variable typ_offset host offs >>-: fun loc -> loc, false),
Alarmset.none
| Mem x ->
- root_forward_eval fuel state x >>=. fun (loc_lv, volatile) ->
+ root_forward_eval context x >>=. fun (loc_lv, volatile) ->
Loc.forward_pointer typ_offset loc_lv offs >>-: fun loc ->
loc, volatile
(* Offset evaluation. Also returns a boolean which is true if the offset
contains a volatile sub-expression. *)
- and eval_offset fuel ~reduce_valid_index typ state = function
- | NoOffset -> return (Loc.no_offset, typ, false)
+ and eval_offset context ~reduce_valid_index typ = function
+ | NoOffset -> return (Loc.no_offset, typ, false)
| Index (index_expr, remaining) ->
let typ_pointed, array_size = match Cil.unrollType typ with
| TArray (t, size, _, _) -> t, size
| t -> Value_parameters.fatal ~current:true
"Got type '%a'" Printer.pp_typ t
in
- eval_offset fuel ~reduce_valid_index typ_pointed state remaining >>=
+ eval_offset context ~reduce_valid_index typ_pointed remaining >>=
fun (roffset, typ_offs, remaining_volatile) ->
- root_forward_eval fuel state index_expr >>= fun (index, volatile) ->
+ root_forward_eval context index_expr >>= fun (index, volatile) ->
let valid_index =
if not (Kernel.SafeArrays.get ()) || not reduce_valid_index
then `Value index, Alarmset.none
@@ -1018,14 +1036,14 @@ module Make
| Field (fi, remaining) ->
let attrs = Cil.filter_qualifier_attributes (Cil.typeAttrs typ) in
let typ_fi = Cil.typeAddAttributes attrs fi.ftype in
- eval_offset fuel ~reduce_valid_index typ_fi state remaining
+ eval_offset context ~reduce_valid_index typ_fi remaining
>>=: fun (r, typ_res, volatile) ->
let off = Loc.forward_field typ fi r in
off, typ_res, volatile
- and eval_lval ?(indeterminate=false) fuel state lval =
+ and eval_lval ?(indeterminate=false) context lval =
(* Computes the location of [lval]. *)
- lval_to_loc fuel ~for_writing:false ~reduction:true state lval
+ lval_to_loc context ~for_writing:false ~reduction:true lval
>>= fun (loc, typ_lv, volatile_expr) ->
let typ_lv = Cil.unrollType typ_lv in
(* the lvalue is volatile:
@@ -1035,8 +1053,8 @@ module Make
*)
let volatile = volatile_expr || Cil.typeHasQualifier "volatile" typ_lv in
(* Find the value of the location, if not bottom. *)
- let oracle = !make_oracle fuel state in
- let v, alarms = Domain.extract_lval oracle state lval typ_lv loc in
+ let oracle = make_oracle context in
+ let v, alarms = Domain.extract_lval oracle context.state lval typ_lv loc in
let alarms = close_dereference_alarms lval alarms in
if indeterminate
then
@@ -1062,35 +1080,55 @@ module Make
(* These two modules could be implemented as mutually recursive, to avoid
the reference for the oracle given to the domains. *)
module Forward_Evaluation = struct
- type state = Domain.t
- let evaluate ?(valuation=Cache.empty) ~fuel state expr =
+ type nonrec context = context
+ let evaluate context valuation expr =
cache := valuation;
- root_forward_eval fuel state expr >>=: fun (value, _) ->
+ root_forward_eval context expr >>=: fun (value, _) ->
!cache, value
end
module Subdivided_Evaluation =
Subdivided_evaluation.Make (Value) (Loc) (Cache) (Forward_Evaluation)
- let () =
- make_oracle :=
- fun fuel state ->
- let fuel = pred fuel in
- if fuel > 0
- then
- fun expr ->
- let valuation = !cache in
- Subdivided_Evaluation.evaluate ~valuation ~fuel state expr
- >>=: fun (valuation, value) ->
- cache := valuation;
- value
- else
- fun _ -> fuel_consumed := true; `Value Value.top, Alarmset.all
+ let oracle context =
+ let remaining_fuel = pred context.remaining_fuel in
+ if remaining_fuel > 0
+ then
+ fun expr ->
+ let valuation = !cache in
+ let context = { context with remaining_fuel } in
+ let subdivnb = context.subdivision in
+ Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
+ >>=: fun (valuation, value) ->
+ cache := valuation;
+ value
+ else
+ fun _ -> fuel_consumed := true; `Value Value.top, Alarmset.all
+
+ (* Context for the forward evaluation of a root expression in state [state]
+ with maximal precision. *)
+ let root_context ?subdivnb state =
+ let remaining_fuel = root_fuel () in
+ (* By default, use the number of subdivision defined by the global option
+ -eva-subdivide-non-linear. *)
+ let subdivision =
+ match subdivnb with
+ | None -> Value_parameters.LinearLevel.get ()
+ | Some n -> n
+ in
+ { state; subdivision; remaining_fuel; oracle }
- let subdivided_forward_eval valuation state expr =
- let fuel = root_fuel () in
- Subdivided_Evaluation.evaluate ~valuation ~fuel state expr
+ (* Context for a fast forward evaluation with minimal precision:
+ no subdivisions and no calls to the oracle. *)
+ let fast_eval_context state =
+ let remaining_fuel = no_fuel in
+ let subdivision = 0 in
+ { state; subdivision; remaining_fuel; oracle }
+ let subdivided_forward_eval valuation ?subdivnb state expr =
+ let context = root_context ?subdivnb state in
+ let subdivnb = context.subdivision in
+ Subdivided_Evaluation.evaluate context valuation ~subdivnb expr
(* ------------------------------------------------------------------------
Backward Evaluation
@@ -1122,7 +1160,7 @@ module Make
let evaluate_for_reduction state expr =
try `Value (Cache.find' !cache expr)
with Not_found ->
- fst (forward_eval no_fuel state expr) >>-: fun _ ->
+ fst (forward_eval (fast_eval_context state) expr) >>-: fun _ ->
try Cache.find' !cache expr
with Not_found -> assert false
@@ -1314,7 +1352,8 @@ module Make
| _ ->
let reduce_valid_index = true in
let typ_lval = Cil.typeOf_pointed (Cil.typeOf expr) in
- fst (eval_offset no_fuel ~reduce_valid_index typ_lval state offset)
+ let context = fast_eval_context state in
+ fst (eval_offset context ~reduce_valid_index typ_lval offset)
>>- fun (loc_offset, _, _) ->
find_val expr >>- fun value ->
Loc.backward_pointer value loc_offset location
@@ -1330,7 +1369,8 @@ module Make
| Index (exp, remaining) ->
find_val exp >>- fun v ->
let typ_pointed = Cil.typeOf_array_elem typ in
- fst (eval_offset no_fuel ~reduce_valid_index:true typ_pointed state remaining)
+ let context = fast_eval_context state in
+ fst (eval_offset context ~reduce_valid_index:true typ_pointed remaining)
>>- fun (rem, _, _) ->
Loc.backward_index typ_pointed v rem loc_offset >>- fun (v', rem') ->
let reduced_v = if Value.is_included v v' then None else Some v' in
@@ -1370,7 +1410,7 @@ module Make
match expr.enode with
| Lval lval -> second_eval_lval state lval value
| _ ->
- fst (internal_forward_eval no_fuel state expr)
+ fst (internal_forward_eval (fast_eval_context state) expr)
>>-: fun (v, _, _) -> v
in
new_value >>- fun evaled ->
@@ -1394,8 +1434,9 @@ module Make
if (fst report).reduction = Backward
then
let for_writing = false
- and reduction = true in
- fst (reduced_lval_to_loc no_fuel ~for_writing ~reduction state lval)
+ and reduction = true
+ and context = fast_eval_context state in
+ fst (reduced_lval_to_loc context ~for_writing ~reduction lval)
>>-: fun (loc, _, _, _) ->
(* TODO: Loc.narrow *)
let record = { record with loc } in
@@ -1407,7 +1448,7 @@ module Make
else `Value ()
in
evaloc >>- fun () ->
- fst (eval_lval no_fuel state lval) >>- fun (record, _, _) ->
+ fst (eval_lval (fast_eval_context state) lval) >>- fun (record, _, _) ->
record.value.v
and recursive_descent state expr =
@@ -1442,8 +1483,8 @@ module Make
module Valuation = Cache
- let evaluate ?(valuation=Cache.empty) ?(reduction=true) state expr =
- let eval, alarms = subdivided_forward_eval valuation state expr in
+ let evaluate ?(valuation=Cache.empty) ?(reduction=true) ?subdivnb state expr =
+ let eval, alarms = subdivided_forward_eval valuation ?subdivnb state expr in
let result =
if not reduction || Alarmset.is_empty alarms
then eval
@@ -1455,17 +1496,17 @@ module Make
in
result, alarms
- let copy_lvalue ?(valuation=Cache.empty) state lval =
+ let copy_lvalue ?(valuation=Cache.empty) ?subdivnb state lval =
let expr = Value_util.lval_to_exp lval
- and fuel = root_fuel () in
+ and context = root_context ?subdivnb state in
try
let record, report = Cache.find' valuation expr in
- if less_fuel_than fuel report.fuel
+ if less_fuel_than context.remaining_fuel report.fuel
then `Value (valuation, record.value), record.val_alarms
else raise Not_found
with Not_found ->
cache := valuation;
- eval_lval ~indeterminate:true fuel state lval
+ eval_lval context ~indeterminate:true lval
>>=: fun (record, _, volatile) ->
let record = reduce_value record in
(* Cache the computed result with an appropriate report. *)
@@ -1477,29 +1518,30 @@ module Make
(* When evaluating an lvalue, we use the subdivided evaluation for the
expressions included in the lvalue. *)
- let rec evaluate_offsets valuation state = function
+ let rec evaluate_offsets valuation ?subdivnb state = function
| NoOffset -> `Value valuation, Alarmset.none
- | Field (_, offset) -> evaluate_offsets valuation state offset
+ | Field (_, offset) -> evaluate_offsets valuation ?subdivnb state offset
| Index (expr, offset) ->
- subdivided_forward_eval valuation state expr
+ subdivided_forward_eval valuation ?subdivnb state expr
>>= fun (valuation, _value) ->
- evaluate_offsets valuation state offset
+ evaluate_offsets valuation ?subdivnb state offset
- let evaluate_host valuation state = function
+ let evaluate_host valuation ?subdivnb state = function
| Var _ -> `Value valuation, Alarmset.none
| Mem expr ->
- subdivided_forward_eval valuation state expr >>=: fst
+ subdivided_forward_eval valuation ?subdivnb state expr >>=: fst
- let lvaluate ?(valuation=Cache.empty) ~for_writing state lval =
+ let lvaluate ?(valuation=Cache.empty) ?subdivnb ~for_writing state lval =
(* If [for_writing] is true, the location of [lval] is reduced by removing
const bases. Use [for_writing:false] if const bases can be written
through a mutable field or an initializing function. *)
let for_writing = for_writing && not (Cil.is_mutable_or_initialized lval) in
let host, offset = lval in
- evaluate_host valuation state host >>= fun valuation ->
- evaluate_offsets valuation state offset >>= fun valuation ->
+ evaluate_host valuation ?subdivnb state host >>= fun valuation ->
+ evaluate_offsets valuation ?subdivnb state offset >>= fun valuation ->
cache := valuation;
- lval_to_loc (root_fuel ()) ~for_writing ~reduction:true state lval
+ let context = root_context ?subdivnb state in
+ lval_to_loc context ~for_writing ~reduction:true lval
>>=. fun (_, typ, _) ->
backward_lval (backward_fuel ()) state lval >>-: fun _ ->
match Cache.find_loc !cache lval with
@@ -1510,7 +1552,11 @@ module Make
(* Generate [e == 0] *)
let expr = Value_util.normalize_as_cond expr (not positive) in
cache := valuation;
- root_forward_eval (root_fuel ()) state expr >>=. fun (_v, volatile) ->
+ (* Currently, no subdivisions are performed during the forward evaluation
+ in this function, which is used to evaluate the conditions of if(…)
+ statements in the analysis. *)
+ let context = root_context ~subdivnb:0 state in
+ root_forward_eval context expr >>=. fun (_v, volatile) ->
(* Reduce by [(e == 0) == 0] *)
backward_eval (backward_fuel ()) state expr (Some Value.zero)
>>- fun () ->
@@ -1518,7 +1564,9 @@ module Make
with Not_Exact_Reduction ->
(* Avoids reduce_by_cond_enumerate on volatile expressions. *)
if volatile then `Value !cache
- else Subdivided_Evaluation.reduce_by_enumeration !cache state expr false
+ else
+ let context = fast_eval_context state in
+ Subdivided_Evaluation.reduce_by_enumeration context !cache expr false
let assume ?valuation:(valuation=Cache.empty) state expr value =
cache := valuation;
@@ -1554,14 +1602,14 @@ module Make
let expr = Cil.mkBinOp ~loc:expr.eloc Ne expr addr in
fst (reduce ~valuation state expr false)
- let eval_function_exp funcexp ?args state =
+ let eval_function_exp ?subdivnb funcexp ?args state =
match funcexp.enode with
| Lval (Var vinfo, NoOffset) ->
`Value [Globals.Functions.get vinfo, Valuation.empty],
Alarmset.none
| Lval (Mem v, NoOffset) ->
begin
- evaluate state v >>= fun (valuation, value) ->
+ evaluate ?subdivnb state v >>= fun (valuation, value) ->
let kfs, alarm = Value.resolve_functions value in
match kfs with
| `Top -> top_function_pointer funcexp
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index b112178c2ac9cb2e021359f162731a2af1b9c2a3..258657a0c581ec61cb2b63c1ad4bd7b93e91a682 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -47,12 +47,16 @@ module type S = sig
for the expression [expr], and [valuation] contains all the intermediate
results of the evaluation.
- The [valuation] argument is a cache of already computed expressions.
- It is empty by default.
- The [reduction] argument allows deactivating the backward reduction
- performed after the forward evaluation. *)
+ Optional arguments are:
+ - [valuation] is a cache of already computed expressions; empty by default.
+ - [reduction] allows the deactivation of the backward reduction performed
+ after the forward evaluation; true by default.
+ - [subdivnb] is the maximum number of subdivisions performed on non-linear
+ sub-expressions of [expr]. If a lvalue occurs several times in [expr],
+ its value can be split up to [subdivnb] times to gain more precision.
+ Set to the value of the option -eva-subdivide-non-linear by default. *)
val evaluate :
- ?valuation:Valuation.t -> ?reduction:bool ->
+ ?valuation:Valuation.t -> ?reduction:bool -> ?subdivnb:int ->
state -> exp -> (Valuation.t * value) evaluated
(** Computes the value of a lvalue, with possible indeterminateness: the
@@ -60,9 +64,11 @@ module type S = sig
Also returns the alarms resulting of the evaluation of the lvalue location,
and a valuation containing all the intermediate results of the evaluation.
The [valuation] argument is a cache of already computed expressions.
- It is empty by default. *)
+ It is empty by default.
+ [subdivnb] is the maximum number of subdivisions performed on non-linear
+ expressions. *)
val copy_lvalue :
- ?valuation:Valuation.t ->
+ ?valuation:Valuation.t -> ?subdivnb:int ->
state -> lval -> (Valuation.t * value flagged_value) evaluated
(** [lvaluate ~valuation ~for_writing state lval] evaluates the left value
@@ -70,9 +76,11 @@ module type S = sig
but evaluates the lvalue into a location and its type.
The boolean [for_writing] indicates whether the lvalue is evaluated to be
read or written. It is useful for the emission of the alarms, and for the
- reduction of the location. *)
+ reduction of the location.
+ [subdivnb] is the maximum number of subdivisions performed on non-linear
+ expressions (including the possible pointer and offset of the lvalue). *)
val lvaluate :
- ?valuation:Valuation.t -> for_writing:bool ->
+ ?valuation:Valuation.t -> ?subdivnb:int -> for_writing:bool ->
state -> lval -> (Valuation.t * loc * typ) evaluated
(** [reduce ~valuation state expr positive] evaluates the expression [expr]
@@ -96,7 +104,7 @@ module type S = sig
state -> exp -> value -> Valuation.t or_bottom
val eval_function_exp:
- exp -> ?args:exp list -> state ->
+ ?subdivnb:int -> exp -> ?args:exp list -> state ->
(Kernel_function.t * Valuation.t) list evaluated
(** Evaluation of the function argument of a [Call] constructor *)
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 893c66fae14163fbaeb6028bbd0c5caaabc31150..b832e789d36607e4baca8e462c25750d3d8e6abe 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -361,10 +361,8 @@ end
module type Forward_Evaluation = sig
type value
type valuation
- type state
- val evaluate:
- ?valuation:valuation -> fuel:int ->
- state -> exp -> (valuation * value) evaluated
+ type context
+ val evaluate: context -> valuation -> exp -> (valuation * value) evaluated
end
module Make
@@ -646,7 +644,7 @@ module Make
[valuation] is the result of the evaluation of [expr] without subdivision.
This function returns the alarms and the valuation resulting from the
subdivided evaluation. *)
- let subdivide_lvals ~fuel subdivnb valuation state expr subexpr lvals =
+ let subdivide_lvals context valuation subdivnb expr subexpr lvals =
let Hypotheses.L variables = Hypotheses.from_list lvals in
(* Split function for the subvalues of [lvals]. *)
let split = make_split valuation variables in
@@ -661,7 +659,7 @@ module Make
(* Updates [variables] with their new [subvalues]. *)
let valuation = update_variables cleared_valuation variables subvalues in
(* Evaluates [expr] with this new valuation. *)
- let eval, alarms = Eva.evaluate ~fuel ~valuation state expr in
+ let eval, alarms = Eva.evaluate context valuation expr in
let result = eval >>-: snd in
(* Optimization if [subexpr] = [expr]. *)
if eq_equal_subexpr
@@ -704,12 +702,12 @@ module Make
eval_result, alarms
(* Builds the information for an lvalue. *)
- let get_info ~fuel valuation state lval =
+ let get_info context valuation lval =
let lv_expr = Value_util.lval_to_exp lval in
(* Reevaluates the lvalue in the initial state, as its value could have
been reduced in the evaluation of the complete expression, and we cannot
omit the alarms for the removed values. *)
- fst (Eva.evaluate ~fuel ~valuation state lv_expr) >>- fun (valuation, _) ->
+ fst (Eva.evaluate context valuation lv_expr) >>- fun (valuation, _) ->
let lv_record = find_val valuation lv_expr in
lv_record.value.v >>-: fun lv_value ->
{ lval; lv_expr; lv_record; lv_value }
@@ -717,8 +715,8 @@ module Make
(* Makes a list of lvalue information from a list of lvalues. Removes lvalues
whose cvalue is singleton or contains addresses, as we cannot subdivide on
such values. *)
- let make_info_list ~fuel valuation state lvals =
- let get_info = get_info ~fuel valuation state in
+ let make_info_list context valuation lvals =
+ let get_info = get_info context valuation in
let get_info acc lval = Bottom.add_to_list (get_info lval) acc in
let list = List.fold_left get_info [] lvals in
List.filter (fun info -> can_be_subdivided (get_cval info.lv_value)) list
@@ -732,9 +730,9 @@ module Make
| `Value (valuation, result) -> f valuation result alarms
(* Subdivided evaluation of [expr] in state [state]. *)
- let subdivide_evaluation ~fuel subdivnb initial_valuation state expr =
+ let subdivide_evaluation context initial_valuation subdivnb expr =
(* Evaluation of [expr] without subdivision. *)
- let default = Eva.evaluate ~fuel ~valuation:initial_valuation state expr in
+ let default = Eva.evaluate context initial_valuation expr in
default >>> fun valuation result alarms ->
(* Do not try to subdivide if the result is singleton or contains some
pointers: the better_bound heuristic only works on numerical values. *)
@@ -750,7 +748,7 @@ module Make
| (subexpr, lvals) :: tail ->
(* Retrieve necessary information about the lvalues.
Also remove lvalues with pointer or singleton values. *)
- let lvals_info = make_info_list ~fuel initial_valuation state lvals in
+ let lvals_info = make_info_list context initial_valuation lvals in
match lvals_info with
| [] -> subdivide_subexpr tail valuation result alarms
| _ ->
@@ -769,16 +767,15 @@ module Make
Value_parameters.result ~current:true ~once:true ~dkey
"subdividing on %a"
(Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lvals;
- subdivide_lvals ~fuel subdivnb valuation state expr subexpr lvals_info
+ subdivide_lvals context valuation subdivnb expr subexpr lvals_info
>>> subdivide_subexpr tail
in
subdivide_subexpr vars valuation result alarms
- let evaluate ?(valuation=Valuation.empty) ~fuel state expr =
- let subdivnb = Value_parameters.LinearLevel.get () in
+ let evaluate context valuation ~subdivnb expr =
if subdivnb = 0 || not activated
- then Eva.evaluate ~valuation ~fuel state expr
- else subdivide_evaluation ~fuel subdivnb valuation state expr
+ then Eva.evaluate context valuation expr
+ else subdivide_evaluation context valuation subdivnb expr
(* ---------------------- Reduction by enumeration ------------------------ *)
@@ -867,13 +864,13 @@ module Make
let get_influential_exprs valuation expr =
get_influential_vars valuation expr []
- let reduce_by_cond_enumerate valuation state cond positive influentials =
+ let reduce_by_cond_enumerate context valuation cond positive influentials =
(* Test whether the condition [expr] may still be true when the
sub-expression [e] has the value [v]. *)
let condition_may_still_be_true valuation expr record value =
let value = { record.value with v = `Value value } in
let valuation = Valuation.add valuation expr { record with value } in
- let eval, _alarms = Eva.evaluate ~valuation ~fuel:0 state cond in
+ let eval, _alarms = Eva.evaluate context valuation cond in
match eval with
| `Bottom -> false
| `Value (_valuation, value) ->
@@ -917,11 +914,11 @@ module Make
(* If the value module contains no cvalue component, this function is
inoperative. Otherwise, it calls reduce_by_cond_enumerate with the
value accessor for the cvalue component. *)
- let reduce_by_enumeration valuation state expr positive =
+ let reduce_by_enumeration context valuation expr positive =
if activated && Value_parameters.EnumerateCond.get ()
then
get_influential_exprs valuation expr >>- fun split_on ->
- reduce_by_cond_enumerate valuation state expr positive split_on
+ reduce_by_cond_enumerate context valuation expr positive split_on
else `Value valuation
end
diff --git a/src/plugins/value/engine/subdivided_evaluation.mli b/src/plugins/value/engine/subdivided_evaluation.mli
index 71d582bb70d8a4e1f6bda7d6d77b88051d08f994..25ed9703977c7d4aceb7effc7b63fc5df026d93b 100644
--- a/src/plugins/value/engine/subdivided_evaluation.mli
+++ b/src/plugins/value/engine/subdivided_evaluation.mli
@@ -25,31 +25,30 @@
by disjunction on their abstract value, in order to gain precision. *)
open Cil_types
+open Eval
module type Forward_Evaluation = sig
type value
type valuation
- type state
- val evaluate:
- ?valuation:valuation -> fuel:int ->
- state -> exp -> (valuation * value) Eval.evaluated
+ type context
+ val evaluate: context -> valuation -> exp -> (valuation * value) evaluated
end
module Make
(Value : Abstract.Value.External)
(Loc: Abstract_location.S with type value = Value.t)
- (Valuation: Eval.Valuation with type value = Value.t
- and type loc = Loc.location)
+ (Valuation: Valuation with type value = Value.t
+ and type loc = Loc.location)
(Eva: Forward_Evaluation with type value := Value.t
and type valuation := Valuation.t)
: sig
val evaluate:
- ?valuation:Valuation.t -> fuel:int ->
- Eva.state -> exp -> (Valuation.t * Value.t) Eval.evaluated
+ Eva.context -> Valuation.t -> subdivnb:int ->
+ exp -> (Valuation.t * Value.t) evaluated
val reduce_by_enumeration:
- Valuation.t -> Eva.state -> exp -> bool -> Valuation.t Eval.or_bottom
+ Eva.context -> Valuation.t -> exp -> bool -> Valuation.t or_bottom
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index fbceb4deb4c00243c9bd0e24800039c304dbd377..b0ffc5fa32a31a07382e3db6f26eb6203d52ea85 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -90,6 +90,12 @@ let is_determinate kf =
|| (name >= "Frama_C" && name < "Frama_D")
|| Builtins.is_builtin_overridden kf)
+let subdivide_stmt = Value_util.get_subdivision
+
+let subdivide_kinstr = function
+ | Kglobal -> Value_parameters.LinearLevel.get ()
+ | Kstmt stmt -> subdivide_stmt stmt
+
(* Used to disambiguate files for Frama_C_dump_each_file directives. *)
module DumpFileCounters =
State_builder.Hashtbl (Datatype.String.Hashtbl) (Datatype.Int)
@@ -150,18 +156,18 @@ module Make (Abstract: Abstractions.Eva) = struct
(* The three functions below call evaluation functions and notify the user
if they lead to bottom without alarms. *)
- let evaluate_and_check ?valuation state expr =
- let res = Eval.evaluate ?valuation state expr in
+ let evaluate_and_check ?valuation ~subdivnb state expr =
+ let res = Eval.evaluate ?valuation ~subdivnb state expr in
report_unreachability state res "the expression %a" Printer.pp_exp expr;
res
- let lvaluate_and_check ~for_writing ?valuation state lval =
- let res = Eval.lvaluate ~for_writing ?valuation state lval in
+ let lvaluate_and_check ?valuation ~subdivnb ~for_writing state lval =
+ let res = Eval.lvaluate ?valuation ~subdivnb ~for_writing state lval in
report_unreachability state res "the lvalue %a" Printer.pp_lval lval;
res
- let copy_lvalue_and_check ?valuation state lval =
- let res = Eval.copy_lvalue ?valuation state lval in
+ let copy_lvalue_and_check ?valuation ~subdivnb state lval =
+ let res = Eval.copy_lvalue ?valuation ~subdivnb state lval in
report_unreachability state res "the copy of %a" Printer.pp_lval lval;
res
@@ -170,17 +176,18 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------------------------------------------------------------ *)
(* Default assignment: evaluates the right expression. *)
- let assign_by_eval state valuation expr =
- evaluate_and_check ~valuation state expr >>=: fun (valuation, value) ->
+ let assign_by_eval ~subdivnb state valuation expr =
+ evaluate_and_check ~valuation ~subdivnb state expr
+ >>=: fun (valuation, value) ->
Assign value, valuation
(* Assignment by copying the value of a right lvalue. *)
- let assign_by_copy state valuation lval lloc ltyp =
+ let assign_by_copy ~subdivnb state valuation lval lloc ltyp =
(* This code about garbled mix is specific to the Cvalue domain.
Unfortunately, the current API for abstract_domain does not permit
distinguishing between an evaluation or a copy. *)
Locations.Location_Bytes.do_track_garbled_mix false;
- let r = copy_lvalue_and_check ~valuation state lval in
+ let r = copy_lvalue_and_check ~valuation ~subdivnb state lval in
Locations.Location_Bytes.do_track_garbled_mix true;
r >>=: fun (valuation, value) ->
Copy ({lval; lloc; ltyp}, value), valuation
@@ -223,8 +230,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Assignment. *)
let assign_lv_or_ret ~is_ret state kinstr lval expr =
let for_writing = for_writing kinstr in
- let eval, alarms_loc = lvaluate_and_check ~for_writing state lval in
- Alarmset.emit kinstr alarms_loc;
+ let subdivnb = subdivide_kinstr kinstr in
+ let eval, alarms = lvaluate_and_check ~for_writing ~subdivnb state lval in
+ Alarmset.emit kinstr alarms;
match eval with
| `Bottom ->
Kernel.warning ~current:true ~once:true
@@ -241,17 +249,20 @@ module Make (Abstract: Abstractions.Eva) = struct
else None
in
let eval, alarms = match lval_copy with
- | None -> assert (not is_ret); assign_by_eval state valuation expr
+ | None ->
+ assert (not is_ret);
+ assign_by_eval ~subdivnb state valuation expr
| Some right_lval ->
+ let for_writing = false in
(* In case of a copy, checks that the left and right locations are
compatible and that they do not overlap. *)
- lvaluate_and_check ~for_writing:false ~valuation state right_lval
- >>= fun (valuation, right_loc, right_typ) ->
- check_overlap ltyp (lval, lloc) (right_lval, right_loc)
- >>= fun (lloc, right_loc) ->
- if are_compatible lloc right_loc
- then assign_by_copy state valuation right_lval right_loc right_typ
- else assign_by_eval state valuation expr
+ lvaluate_and_check ~for_writing ~subdivnb ~valuation state right_lval
+ >>= fun (valuation, rloc, rtyp) ->
+ check_overlap ltyp (lval, lloc) (right_lval, rloc)
+ >>= fun (lloc, rloc) ->
+ if are_compatible lloc rloc
+ then assign_by_copy ~subdivnb state valuation right_lval rloc rtyp
+ else assign_by_eval ~subdivnb state valuation expr
in
if is_ret then assert (Alarmset.is_empty alarms);
Alarmset.emit kinstr alarms;
@@ -387,7 +398,7 @@ module Make (Abstract: Abstractions.Eva) = struct
If the call has copied the argument, it may be uninitialized. Thus,
we also avoid the backward propagation if the formal is uninitialized
here. This should not happen in the Assign case above. *)
- fst (Eval.copy_lvalue ~valuation:empty state lval)
+ fst (Eval.copy_lvalue ~valuation:empty ~subdivnb:0 state lval)
>>- fun (_valuation, post_value) ->
if
Bottom.is_included Value.is_included pre_value post_value.v
@@ -491,10 +502,10 @@ module Make (Abstract: Abstractions.Eva) = struct
evaluates the call argument [expr] in the state [state] and the valuation
[valuation]. Returns the value assigned, and the updated valuation.
TODO: share more code with [assign]. *)
- let evaluate_actual ~determinate valuation state expr =
+ let evaluate_actual ~subdivnb ~determinate valuation state expr =
match expr.enode with
| Lval lv ->
- lvaluate_and_check ~for_writing:false ~valuation state lv
+ lvaluate_and_check ~for_writing:false ~subdivnb ~valuation state lv
>>= fun (valuation, loc, typ) ->
if Int_Base.is_top (Location.size loc)
then
@@ -502,18 +513,17 @@ module Make (Abstract: Abstractions.Eva) = struct
"Function argument %a has unknown size. Aborting"
Printer.pp_exp expr;
if determinate && Cil.isArithmeticOrPointerType (Cil.typeOfLval lv)
- then assign_by_eval state valuation expr
- else assign_by_copy state valuation lv loc typ
- | _ ->
- assign_by_eval state valuation expr
+ then assign_by_eval ~subdivnb state valuation expr
+ else assign_by_copy ~subdivnb state valuation lv loc typ
+ | _ -> assign_by_eval ~subdivnb state valuation expr
(* Evaluates the list of the actual arguments of a call. Returns the list
of each argument expression associated to its assigned value, and the
valuation resulting of the evaluations. *)
- let compute_actuals determinate valuation state arguments =
+ let compute_actuals ~subdivnb ~determinate valuation state arguments =
let process expr acc =
acc >>= fun (args, valuation) ->
- evaluate_actual ~determinate valuation state expr >>=:
+ evaluate_actual ~subdivnb ~determinate valuation state expr >>=:
fun (assigned, valuation) ->
(expr, assigned) :: args, valuation
in
@@ -548,10 +558,10 @@ module Make (Abstract: Abstractions.Eva) = struct
in
{kf; arguments; rest; return; recursive}
- let make_call kf arguments valuation state =
+ let make_call ~subdivnb kf arguments valuation state =
(* Evaluate the arguments of the call. *)
let determinate = is_determinate kf in
- compute_actuals determinate valuation state arguments
+ compute_actuals ~subdivnb ~determinate valuation state arguments
>>=: fun (args, valuation) ->
let call = create_call kf args in
call, valuation
@@ -589,10 +599,10 @@ module Make (Abstract: Abstractions.Eva) = struct
else fun _ _ _ _ -> ()
(* Frama_C_domain_show_each functions. *)
- let domain_show_each name arguments state =
+ let domain_show_each ~subdivnb name arguments state =
let pretty fmt expr =
let pp fmt =
- match fst (Eval.evaluate state expr) with
+ match fst (Eval.evaluate ~subdivnb state expr) with
| `Bottom -> Format.fprintf fmt "%s" (Unicode.bottom_string ())
| `Value (valuation, _value) -> show_expr valuation state fmt expr
in
@@ -607,15 +617,15 @@ module Make (Abstract: Abstractions.Eva) = struct
let show_offsm =
match Domain.get_cvalue, Location.get Main_locations.PLoc.key with
| None, _ | _, None ->
- fun fmt _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
+ fun fmt _ _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cvalue, Some get_ploc ->
- fun fmt expr state ->
+ fun fmt subdivnb expr state ->
match expr.enode with
| Lval lval ->
begin
try
let offsm =
- fst (Eval.lvaluate ~for_writing:false state lval)
+ fst (Eval.lvaluate ~for_writing:false ~subdivnb state lval)
>>- fun (_, loc, _) ->
Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
in
@@ -629,28 +639,30 @@ module Make (Abstract: Abstractions.Eva) = struct
(* For scalar expressions, prints the cvalue component of their values. *)
let show_value =
match Value.get Main_values.CVal.key with
- | None -> fun fmt _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
+ | None -> fun fmt _ _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cval ->
- fun fmt expr state ->
- let value = fst (Eval.evaluate state expr) >>-: snd >>-: get_cval in
+ fun fmt subdivnb expr state ->
+ let value =
+ fst (Eval.evaluate ~subdivnb state expr) >>-: snd >>-: get_cval
+ in
(Bottom.pretty Cvalue.V.pretty) fmt value
- let pretty_arguments state arguments =
+ let pretty_arguments ~subdivnb state arguments =
let pretty fmt expr =
if Cil.isArithmeticOrPointerType (Cil.typeOf expr)
- then show_value fmt expr state
- else show_offsm fmt expr state
+ then show_value fmt subdivnb expr state
+ else show_offsm fmt subdivnb expr state
in
Pretty_utils.pp_list ~pre:"@[<hv>" ~sep:",@ " ~suf:"@]" pretty arguments
(* Frama_C_show_each functions. *)
- let show_each name arguments state =
+ let show_each ~subdivnb name arguments state =
Value_parameters.result ~current:true
"@[<hv>%s:@ %a@]%t"
- name (pretty_arguments state) arguments Value_util.pp_callstack
+ name (pretty_arguments ~subdivnb state) arguments Value_util.pp_callstack
(* Frama_C_dump_each_file functions. *)
- let dump_state_file_exc name arguments state =
+ let dump_state_file_exc ~subdivnb name arguments state =
let size = String.length name in
let name =
if size > 23
@@ -669,29 +681,30 @@ module Make (Abstract: Abstractions.Eva) = struct
Format.fprintf fmt "DUMPING STATE at file %a line %d@."
Datatype.Filepath.pretty l.Filepath.pos_path
l.Filepath.pos_lnum;
+ let pretty_args = pretty_arguments ~subdivnb state in
if arguments <> []
- then Format.fprintf fmt "Args: %a@." (pretty_arguments state) arguments;
+ then Format.fprintf fmt "Args: %a@." pretty_args arguments;
Format.fprintf fmt "@[<v>%a@]@?" print_state state;
close_out ch
- let dump_state_file name arguments state =
- try dump_state_file_exc name arguments state
+ let dump_state_file ~subdivnb name arguments state =
+ try dump_state_file_exc ~subdivnb name arguments state
with e ->
Value_parameters.warning ~current:true ~once:true
"Error during, or invalid call to Frama_C_dump_each_file (%s). Ignoring"
(Printexc.to_string e)
(** Applies the show_each or dump_each directives. *)
- let apply_special_directives kf arguments state =
+ let apply_special_directives ~subdivnb kf arguments state =
let name = Kernel_function.get_name kf in
if Ast_info.can_be_cea_function name
then
if Ast_info.is_cea_function name
- then (show_each name arguments state; true)
+ then (show_each ~subdivnb name arguments state; true)
else if Ast_info.is_cea_domain_function name
- then (domain_show_each name arguments state; true)
+ then (domain_show_each ~subdivnb name arguments state; true)
else if Ast_info.is_cea_dump_file_function name
- then (dump_state_file name arguments state; true)
+ then (dump_state_file ~subdivnb name arguments state; true)
else if Ast_info.is_cea_dump_function name
then (dump_state name state; true)
else false
@@ -719,22 +732,25 @@ module Make (Abstract: Abstractions.Eva) = struct
let call stmt lval_option funcexp args state =
let ki_call = Kstmt stmt in
+ let subdivnb = subdivide_stmt stmt in
+ (* Resolve [funcexp] into the called kernel functions. *)
+ let functions, alarms =
+ Eval.eval_function_exp ~subdivnb funcexp ~args state
+ in
+ Alarmset.emit ki_call alarms;
let cacheable = ref Value_types.Cacheable in
let eval =
- (* Resolve [funcexp] into the called kernel functions. *)
- let functions, alarms = Eval.eval_function_exp funcexp ~args state in
- Alarmset.emit ki_call alarms;
functions >>- fun functions ->
let current_kf = Value_util.current_kf () in
let process_one_function kf valuation =
(* The special Frama_C_ functions to print states are handled here. *)
- if apply_special_directives kf args state
+ if apply_special_directives ~subdivnb kf args state
then
let () = apply_cvalue_callback kf ki_call state in
`Value ([state])
else
(* Create the call. *)
- let eval, alarms = make_call kf args valuation state in
+ let eval, alarms = make_call ~subdivnb kf args valuation state in
Alarmset.emit ki_call alarms;
eval >>- fun (call, valuation) ->
(* Register the call. *)
@@ -771,8 +787,11 @@ module Make (Abstract: Abstractions.Eva) = struct
| `True | `TrueReduced _ -> Alarmset.none
let check_non_overlapping state lvs1 lvs2 =
+ let lvaluate ~valuation lval =
+ fst (Eval.lvaluate ~valuation ~for_writing:false ~subdivnb:0 state lval)
+ in
let eval_loc (acc, valuation) lval =
- match fst (Eval.lvaluate ~valuation ~for_writing:false state lval) with
+ match lvaluate ~valuation lval with
| `Bottom -> acc, valuation
| `Value (valuation, loc, _) -> (lval, loc) :: acc, valuation
in
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index eb378dc20bbd738c1af9512c6a722d57450098c7..87940525f00a5e3dc17b9724c26d5883ef0c1078 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -229,6 +229,9 @@ struct
(* Domains transfer functions. *)
module TF = Abstract.Dom.Transfer (Abstract.Eval.Valuation)
+ (* Evaluation with no reduction and no subdivision. *)
+ let evaluate = Abstract.Eval.evaluate ~reduction:false ~subdivnb:0
+
exception Operation_failed
let fail ~exp message =
@@ -239,10 +242,10 @@ struct
in
Pretty_utils.ksfprintf warn_and_raise message
- let evaluate_exp_to_ival ?valuation state exp =
+ let evaluate_exp_to_ival state exp =
(* Evaluate the expression *)
let valuation, value =
- match Abstract.Eval.evaluate ?valuation ~reduction:false state exp with
+ match evaluate state exp with
| `Value (valuation, value), alarms when Alarmset.is_empty alarms ->
valuation, value
| _ ->
@@ -336,7 +339,7 @@ struct
let typ = Cil.typeOf expr in
let make stamp i = stamp, i, Abstract.Val.inject_int typ i in
let expected_values = List.mapi make expected_values in
- match fst (Abstract.Eval.evaluate state expr) with
+ match fst (evaluate state expr) with
| `Bottom -> None
| `Value (_cache, value) ->
let is_included (_, _, v) = Abstract.Val.is_included v value in
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 33ad321a5cba2cdbbf4c053b7f77fb153a91656b..6b5a0bee6b8a079dd2ac24d98997e3a05d406f1f 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Value_parameters
-open Partitioning_annots
+open Eva_annotations
open Cil_types
let is_return s = match s.skind with Return _ -> true | _ -> false
diff --git a/src/plugins/value/partitioning/per_stmt_slevel.ml b/src/plugins/value/partitioning/per_stmt_slevel.ml
index ca504df3baeb37c32d6aa5048117373d27e3afb6..d93674f6e63b5429a3a18fb2dd1b76c992117c48 100644
--- a/src/plugins/value/partitioning/per_stmt_slevel.ml
+++ b/src/plugins/value/partitioning/per_stmt_slevel.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
open Cil_types
-open Partitioning_annots
+open Eva_annotations
module G = struct
type t = kernel_function
diff --git a/src/plugins/value/utils/partitioning_annots.ml b/src/plugins/value/utils/eva_annotations.ml
similarity index 91%
rename from src/plugins/value/utils/partitioning_annots.ml
rename to src/plugins/value/utils/eva_annotations.ml
index 804c3c8e15f37979764c7bd0e1194606339a5261..767cf487636ff235b6e01cd46d9b498eb3c9c624 100644
--- a/src/plugins/value/utils/partitioning_annots.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -224,3 +224,30 @@ let add_unroll_annot = Unroll.add
let add_flow_annot ~emitter ~loc stmt = function
| FlowSplit annot -> Split.add ~emitter ~loc stmt annot
| FlowMerge annot -> Merge.add ~emitter ~loc stmt annot
+
+
+module Subdivision = Register (struct
+ type t = int
+ let name = "subdivide"
+ let is_loop_annot = false
+
+ let parse ~typing_context:_ = function
+ | [{lexpr_node = PLconstant (IntConstant i)}] ->
+ let i =
+ try int_of_string i
+ with Failure _ -> raise Parse_error
+ in
+ if i < 0 then raise Parse_error;
+ i
+ | _ -> raise Parse_error
+
+ let export i = Ext_terms [Logic_const.tinteger i]
+ let import = function
+ | Ext_terms [{term_node = TConst (Integer (i, _))}] -> Integer.to_int i
+ | _ -> assert false
+
+ let print fmt i = Format.pp_print_int fmt i
+ end)
+
+let get_subdivision_annot = Subdivision.get
+let add_subdivision_annot = Subdivision.add
diff --git a/src/plugins/value/utils/partitioning_annots.mli b/src/plugins/value/utils/eva_annotations.mli
similarity index 82%
rename from src/plugins/value/utils/partitioning_annots.mli
rename to src/plugins/value/utils/eva_annotations.mli
index a95de0105a702588333f4b03f8d12a7da496211e..9c29a1612aa26943e112d925fe38fce12502be31 100644
--- a/src/plugins/value/utils/partitioning_annots.mli
+++ b/src/plugins/value/utils/eva_annotations.mli
@@ -20,6 +20,14 @@
(* *)
(**************************************************************************)
+(** Registers Eva annotations:
+ - slevel annotations: "slevel default", "slevel merge" and "slevel i"
+ - loop unroll annotations: "loop unroll term"
+ - value partitioning annotations: "split term" and "merge term"
+ - subdivision annotations: "subdivide i"
+
+ Widen hints annotations are still registered in !{widen_hints_ext.ml}. *)
+
type slevel_annotation =
| SlevelMerge
| SlevelDefault
@@ -34,6 +42,7 @@ type flow_annotation =
val get_slevel_annot : Cil_types.stmt -> slevel_annotation option
val get_unroll_annot : Cil_types.stmt -> unroll_annotation list
val get_flow_annot : Cil_types.stmt -> flow_annotation list
+val get_subdivision_annot : Cil_types.stmt -> int list
val add_slevel_annot : emitter:Emitter.t -> loc:Cil_types.location ->
Cil_types.stmt -> slevel_annotation -> unit
@@ -41,3 +50,5 @@ val add_unroll_annot : emitter:Emitter.t -> loc:Cil_types.location ->
Cil_types.stmt -> unroll_annotation -> unit
val add_flow_annot : emitter:Emitter.t -> loc:Cil_types.location ->
Cil_types.stmt -> flow_annotation -> unit
+val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
+ Cil_types.stmt -> int -> unit
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 99bfd13838fb8991f534a2720753c88bf5b1a6e7..545c6bfc12471b277f1da3c25e57623db1b473ae 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -71,6 +71,22 @@ let get_slevel kf =
try Value_parameters.SlevelFunction.find kf
with Not_found -> Value_parameters.SemanticUnrollingLevel.get ()
+let get_subdivision_option stmt =
+ try
+ let kf = Kernel_function.find_englobing_kf stmt in
+ Value_parameters.LinearLevelFunction.find kf
+ with Not_found -> Value_parameters.LinearLevel.get ()
+
+let get_subdivision stmt =
+ match Eva_annotations.get_subdivision_annot stmt with
+ | [] -> get_subdivision_option stmt
+ | [x] -> x
+ | x :: _ ->
+ Value_parameters.warning ~current:true ~once:true
+ "Several subdivision annotations at the same statement; selecting %i\
+ and ignoring the others." x;
+ x
+
let pretty_actuals fmt actuals =
let pp fmt (e,x,_) = Cvalue.V.pretty_typ (Some (Cil.typeOf e)) fmt x in
Pretty_utils.pp_flowlist pp fmt actuals
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index a631d797987bfab295360fc4b9e837bcaf042922..1613ca7b695c8eebe6278f633f1495e48795e6dd 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -46,6 +46,7 @@ val pp_callstack : Format.formatter -> unit
(* TODO: Document the rest of this file. *)
val emitter : Emitter.t
val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
+val get_subdivision: stmt -> int
val pretty_actuals :
Format.formatter -> (Cil_types.exp * Cvalue.V.t * 'b) list -> unit
val pretty_current_cfunction_name : Format.formatter -> unit
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 6213ef4f51156fcaffba7d0fd7c1e0a9306a9f4b..a56b71755be5a1106cbe0d50d70965a98076504a 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -1020,6 +1020,30 @@ module LinearLevel =
let () = add_precision_dep LinearLevel.parameter
let () = LinearLevel.add_aliases ["-val-subdivide-non-linear"]
+let () = Parameter_customize.set_group precision_tuning
+module LinearLevelFunction =
+ Kernel_function_map
+ (struct
+ include Datatype.Int
+ type key = Cil_types.kernel_function
+ let of_string ~key:_ ~prev:_ s =
+ Extlib.opt_map
+ (fun s ->
+ try int_of_string s
+ with Failure _ ->
+ raise (Cannot_build ("'" ^ s ^ "' is not an integer")))
+ s
+ let to_string ~key:_ = Extlib.opt_map string_of_int
+ end)
+ (struct
+ let option_name = "-eva-subdivide-non-linear-function"
+ let arg_name = "f:n"
+ let help = "override the global option -eva-subdivide-non-linear with <n>\
+ when analyzing the function <f>."
+ let default = Kernel_function.Map.empty
+ end)
+let () = add_precision_dep LinearLevelFunction.parameter
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
module UsePrototype =
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 00db23383f500a22b368d1c34a279ef972cd07ee..f4a069d86ed4859e3deec979674f55ed24463f52 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -129,6 +129,10 @@ module SkipLibcSpecs: Parameter_sig.Bool
module RmAssert: Parameter_sig.Bool
module LinearLevel: Parameter_sig.Int
+module LinearLevelFunction:
+ Parameter_sig.Map with type key = Cil_types.kernel_function
+ and type value = int
+
module BuiltinsOverrides:
Parameter_sig.Map with type key = Cil_types.kernel_function
and type value = string
diff --git a/tests/value/nonlin.c b/tests/value/nonlin.c
index 173929f555a96b0ca01f8e7585879fb4895598af..7395d9b0d4b5940e73762857645d559c76835fe9 100644
--- a/tests/value/nonlin.c
+++ b/tests/value/nonlin.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-eva-subdivide-non-linear 14 -eva-msg-key nonlin"
+ STDOPT: +"-eva-subdivide-non-linear 14 -eva-subdivide-non-linear-function=local_subdivide:32 -eva-msg-key nonlin"
*/
#include "__fc_builtin.h"
@@ -103,10 +103,25 @@ void subdivide_reduced_value () {
int r = t1[i] - t2[i];
}
+/* Tests local subdivision via option -eva-subdivide-non-linear-function
+ and annotations subdivide. */
+void local_subdivide () {
+ int x = Frama_C_interval(-10, 10);
+ int y = Frama_C_interval(-10, 10);
+ /*@ subdivide 0; */
+ int imprecise = x*x - 2*x*y + y*y; // No subdivision: [-400..400]
+ /*@ subdivide 14; */
+ int more_precise = x*x - 2*x*y + y*y; // Some subdivisions: [-48..400]
+ int even_more_precise = x*x - 2*x*y + y*y; // Local subdivision: [-16..400]
+ /*@ subdivide 100; */
+ int precise = x*x - 2*x*y + y*y; // Maximal subdivision: [0..400]
+}
+
void main () {
subdivide_integer ();
subdivide_pointer ();
subdivide_several_variables ();
if (v) subdivide_table ();
subdivide_reduced_value ();
+ local_subdivide ();
}
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index 14387a41a7e3291ac05201ac0be199a89d76142a..ca1b870962dc9a89c3d58e9d29bea23a70cbdfec 100644
--- a/tests/value/oracle/nonlin.res.oracle
+++ b/tests/value/oracle/nonlin.res.oracle
@@ -24,7 +24,7 @@
[31] ∈ {5}
[32..35] ∈ {0}
[eva] computing for function subdivide_integer <- main.
- Called from tests/value/nonlin.c:107.
+ Called from tests/value/nonlin.c:121.
[eva:nonlin] tests/value/nonlin.c:31:
non-linear '((int)z + 675) * ((int)z + 675)', lv 'z'
[eva:nonlin] tests/value/nonlin.c:31: subdividing on z
@@ -45,7 +45,7 @@
[eva] Recording results for subdivide_integer
[eva] Done for function subdivide_integer
[eva] computing for function subdivide_pointer <- main.
- Called from tests/value/nonlin.c:108.
+ Called from tests/value/nonlin.c:122.
[eva] computing for function Frama_C_interval <- subdivide_pointer <- main.
Called from tests/value/nonlin.c:12.
[eva] using specification for function Frama_C_interval
@@ -68,7 +68,7 @@
[eva] Recording results for subdivide_pointer
[eva] Done for function subdivide_pointer
[eva] computing for function subdivide_several_variables <- main.
- Called from tests/value/nonlin.c:109.
+ Called from tests/value/nonlin.c:123.
[eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main.
Called from tests/value/nonlin.c:51.
@@ -117,7 +117,7 @@
[eva] Recording results for subdivide_several_variables
[eva] Done for function subdivide_several_variables
[eva] computing for function subdivide_table <- main.
- Called from tests/value/nonlin.c:110.
+ Called from tests/value/nonlin.c:124.
[eva] tests/value/nonlin.c:89: loop invariant got status valid.
[eva] tests/value/nonlin.c:90: starting to merge loop iterations
[eva:nonlin] tests/value/nonlin.c:91:
@@ -126,7 +126,7 @@
[eva] Recording results for subdivide_table
[eva] Done for function subdivide_table
[eva] computing for function subdivide_reduced_value <- main.
- Called from tests/value/nonlin.c:111.
+ Called from tests/value/nonlin.c:125.
[eva:nonlin] tests/value/nonlin.c:103: non-linear 't1[i] - t2[i]', lv 'i'
[eva:nonlin] tests/value/nonlin.c:103: subdividing on i
[eva:alarm] tests/value/nonlin.c:103: Warning:
@@ -135,9 +135,36 @@
accessing out of bounds index. assert i < 2;
[eva] Recording results for subdivide_reduced_value
[eva] Done for function subdivide_reduced_value
+[eva] computing for function local_subdivide <- main.
+ Called from tests/value/nonlin.c:126.
+[eva] computing for function Frama_C_interval <- local_subdivide <- main.
+ Called from tests/value/nonlin.c:109.
+[eva] tests/value/nonlin.c:109:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- local_subdivide <- main.
+ Called from tests/value/nonlin.c:110.
+[eva] tests/value/nonlin.c:110:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:nonlin] tests/value/nonlin.c:114:
+ non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x'
+[eva:nonlin] tests/value/nonlin.c:114: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:115: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:117: subdividing on x, y
+[eva] Recording results for local_subdivide
+[eva] Done for function local_subdivide
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function local_subdivide:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ [-10..10]
+ y ∈ [-10..10]
+ imprecise ∈ [-400..400]
+ more_precise ∈ [-48..400]
+ even_more_precise ∈ [-16..400]
+ precise ∈ [0..400]
[eva:final-states] Values at end of function subdivide_integer:
z ∈ [-32768..28523]
k ∈ [-2..1118367364]
@@ -180,11 +207,13 @@
NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
+[from] Computing for function local_subdivide
+[from] Computing for function Frama_C_interval <-local_subdivide
+[from] Done for function Frama_C_interval
+[from] Done for function local_subdivide
[from] Computing for function subdivide_integer
[from] Done for function subdivide_integer
[from] Computing for function subdivide_pointer
-[from] Computing for function Frama_C_interval <-subdivide_pointer
-[from] Done for function Frama_C_interval
[from] Done for function subdivide_pointer
[from] Computing for function subdivide_reduced_value
[from] Done for function subdivide_reduced_value
@@ -200,6 +229,8 @@
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
+[from] Function local_subdivide:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function subdivide_integer:
NO EFFECTS
[from] Function subdivide_pointer:
@@ -213,6 +244,11 @@
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function local_subdivide:
+ Frama_C_entropy_source; x; y; imprecise; more_precise; even_more_precise;
+ precise
+[inout] Inputs for function local_subdivide:
+ Frama_C_entropy_source
[inout] Out (internal) for function subdivide_integer:
z; k; l; x; p; i1; i2; r; t[0..100]; idx
[inout] Inputs for function subdivide_integer: