From 2fb335e961cfe6c425dba7b02978feb5edeaa4a8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 21 Jan 2021 18:20:43 +0100
Subject: [PATCH] [aorai] do not propagate \result as a binding to caller
functions...
---
src/plugins/aorai/aorai_dataflow.ml | 78 +++++++++++++++++++---------
src/plugins/aorai/aorai_utils.ml | 2 +
src/plugins/aorai/data_for_aorai.ml | 10 ++++
src/plugins/aorai/data_for_aorai.mli | 1 +
4 files changed, 66 insertions(+), 25 deletions(-)
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index 63a0214b2a2..a556a8a1cd3 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -70,6 +70,7 @@ let compose_range loc b r1 r2 =
->
if Cil.isLogicZero b then Data_for_aorai.absolute_range loc (min1 + min2)
else Unbounded (min1 + min2)
+ | Unknown, _ | _, Unknown -> Unknown
let fail_on_both k elt1 elt2 =
match elt1, elt2 with
@@ -85,8 +86,7 @@ let compose_bindings map1 loc vals map =
let vals = Cil_datatype.Term.Map.fold
(fun base intv vals ->
let vals' =
- if Cil.isLogicZero base then
- Cil_datatype.Term.Map.add base intv Cil_datatype.Term.Map.empty
+ if Cil.isLogicZero base then Cil_datatype.Term.Map.singleton base intv
else
try
let orig_base = Cil_datatype.Term.Map.find base map1 in
@@ -96,8 +96,7 @@ let compose_bindings map1 loc vals map =
Cil_datatype.Term.Map.add base intv' map
)
orig_base Cil_datatype.Term.Map.empty
- with Not_found ->
- Cil_datatype.Term.Map.add base intv Cil_datatype.Term.Map.empty
+ with Not_found -> Cil_datatype.Term.Map.singleton base intv
in
Cil_datatype.Term.Map.merge
(Extlib.merge_opt (Data_for_aorai.merge_range loc)) vals' vals
@@ -273,8 +272,9 @@ let make_start_transition ?(is_main=false) kf init_states =
(fun trans kf -> Aorai_utils.isCrossable trans kf Promelaast.Call)
in
let treat_one_state state acc =
- let my_trans = Path_analysis.get_transitions_of_state state auto in
- let treat_one_trans acc trans =
+ if Data_for_aorai.isObservableFunction kf then begin
+ let my_trans = Path_analysis.get_transitions_of_state state auto in
+ let treat_one_trans acc trans =
if is_crossable trans kf then begin
let bindings = actions_to_range trans.actions in
let fst_set =
@@ -286,13 +286,23 @@ let make_start_transition ?(is_main=false) kf init_states =
add_or_merge trans.stop (fst_set, last_set, bindings) acc
end
else acc
- in
- let possible_states =
- List.fold_left
- treat_one_trans Data_for_aorai.Aorai_state.Map.empty my_trans
- in
- if Data_for_aorai.Aorai_state.Map.is_empty possible_states then acc
- else Data_for_aorai.Aorai_state.Map.add state possible_states acc
+ in
+ let possible_states =
+ List.fold_left
+ treat_one_trans Data_for_aorai.Aorai_state.Map.empty my_trans
+ in
+ if Data_for_aorai.Aorai_state.Map.is_empty possible_states then acc
+ else Data_for_aorai.Aorai_state.Map.add state possible_states acc
+ end else begin
+ (* function is not observed by automaton: this is as if there
+ were a single transition letting the state unchanged. *)
+ Data_for_aorai.Aorai_state.(
+ Map.add state
+ (Map.singleton state
+ (Set.singleton state, Set.singleton state,
+ Cil_datatype.Term.Map.empty))
+ acc)
+ end
in
let res =
Data_for_aorai.Aorai_state.Set.fold
@@ -304,16 +314,28 @@ let make_return_transition kf state =
set_return_state s state;
let auto = Data_for_aorai.getGraph () in
let treat_one_state state bindings acc =
- let my_trans = Path_analysis.get_transitions_of_state state auto in
- let last = Data_for_aorai.Aorai_state.Set.singleton state in
- let treat_one_trans acc trans =
- if Aorai_utils.isCrossable trans kf Promelaast.Return then begin
- let my_bindings = actions_to_range trans.actions in
- let new_bindings = compose_actions bindings (last, last, my_bindings) in
- add_or_merge trans.stop new_bindings acc
- end else acc
- in
- List.fold_left treat_one_trans acc my_trans
+ if Data_for_aorai.isObservableFunction kf then begin
+ let my_trans = Path_analysis.get_transitions_of_state state auto in
+ let last = Data_for_aorai.Aorai_state.Set.singleton state in
+ let treat_one_trans acc trans =
+ if Aorai_utils.isCrossable trans kf Promelaast.Return then begin
+ let my_bindings = actions_to_range trans.actions in
+ let new_bindings =
+ compose_actions bindings (last, last, my_bindings)
+ in
+ add_or_merge trans.stop new_bindings acc
+ end else acc
+ in
+ List.fold_left treat_one_trans acc my_trans
+ end else begin
+ (* non-observable function: its return does not change the state
+ of the automaton. *)
+ let last = Data_for_aorai.Aorai_state.Set.singleton state in
+ let new_bindings =
+ compose_actions bindings (last,last,Cil_datatype.Term.Map.empty)
+ in
+ add_or_merge state new_bindings acc
+ end
in
let treat_one_path start_state curr_state acc =
let res =
@@ -430,7 +452,7 @@ module Computer(I: Init) = struct
let do_call s f args (state,loops as d) =
let kf = Globals.Functions.get f in
- if not (Data_for_aorai.isObservableFunction kf)
+ if Data_for_aorai.isIgnoredFunction kf
then d (* we simply skip ignored functions. *)
else begin
set_call_state s state;
@@ -455,7 +477,13 @@ module Computer(I: Init) = struct
let acc = Cil_datatype.Term.Map.add lv value acc in
bind acc prms args
in
- let args = bind Cil_datatype.Term.Map.empty prms args in
+ let res = Logic_const.tresult (Kernel_function.get_return_type kf) in
+ let z = Logic_const.tinteger 0 in
+ (* invalidate bindings to \result of the callee.
+ TODO: generate global variable to store the result if needed?
+ *)
+ let map = Cil_datatype.Term.Map.(singleton res (singleton z Unknown)) in
+ let args = bind map prms args in
let init_states = extract_current_states state in
let init_trans = make_start_transition kf init_states in
let end_state = !compute_func I.stack (Kstmt s) kf init_trans in
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 7f31429c31e..d1c5ef527a9 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -2200,6 +2200,8 @@ let treat_val loc base range pred =
let max = Logic_const.prel (Rle, loc, add max) in
Logic_const.pand (min,max)
| Unbounded min -> Logic_const.prel (Rle, add_cst min, loc)
+ | Unknown -> Logic_const.ptrue (* nothing is known: the loc can
+ take any value from then on. *)
in
Aorai_option.debug ~dkey:action_dkey "Action predicate: %a"
Printer.pp_predicate res;
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 70b4551cbd7..b18b1886af1 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -1755,6 +1755,7 @@ type range =
*)
| Unbounded of int (** only the lower bound is known,
there is no upper bound *)
+ | Unknown (** completely unknown value. *)
module Range = Datatype.Make_with_collections
(struct
@@ -1782,11 +1783,15 @@ module Range = Datatype.Make_with_collections
| Bounded _, _ -> 1
| _, Bounded _ -> -1
| Unbounded c1, Unbounded c2 -> Datatype.Int.compare c1 c2
+ | Unbounded _, _ -> 1
+ | _, Unbounded _ -> -1
+ | Unknown, Unknown -> 0
let hash = function
| Fixed c1 -> 2 * c1
| Interval(c1,c2) -> 3 * (c1 + c2)
| Bounded (c1,c2) -> 5 * (c1 + Cil_datatype.Term.hash c2)
| Unbounded c1 -> 7 * c1
+ | Unknown -> 11
let copy = function
| Fixed c1 ->
Fixed (Datatype.Int.copy c1)
@@ -1795,6 +1800,7 @@ module Range = Datatype.Make_with_collections
| Bounded(c1,c2) ->
Bounded(Datatype.Int.copy c1, Cil_datatype.Term.copy c2)
| Unbounded c1 -> Unbounded (Datatype.Int.copy c1)
+ | Unknown -> Unknown
let internal_pretty_code _ = Datatype.from_pretty_code
let pretty fmt = function
| Fixed c1 -> Format.fprintf fmt "%d" c1
@@ -1804,6 +1810,7 @@ module Range = Datatype.Make_with_collections
Format.fprintf fmt "@[<2>[%d..@;%a]@]" c1
Cil_datatype.Term.pretty c2
| Unbounded c1 -> Format.fprintf fmt "[%d..]" c1
+ | Unknown -> Format.fprintf fmt "[..]"
let varname _ = "r"
let mem_project = Datatype.never_any_project
end)
@@ -1879,6 +1886,7 @@ let merge_range loc base r1 r2 =
let min =
if Datatype.Int.compare min2 min1 < 0 then min2 else min1
in Unbounded min
+ | Unknown, _ | _, Unknown -> Unknown
let tlval lv = Logic_const.term (TLval lv) (Cil.typeOfTermLval lv)
@@ -1900,6 +1908,8 @@ let included_range range1 range2 =
| Bounded(l1,_), Unbounded l2 -> Datatype.Int.compare l1 l2 <= 0
| Unbounded l1, Unbounded l2 -> Datatype.Int.compare l1 l2 <= 0
| Unbounded _, (Fixed _ | Interval _ | Bounded _) -> false
+ | _, Unknown -> true
+ | Unknown, _ -> false
let unchanged loc =
Cil_datatype.Term.Map.add loc (Fixed 0) Cil_datatype.Term.Map.empty
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 603579cd90d..71ecd72e175 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -301,6 +301,7 @@ type range =
(** range bounded by a logic term (depending on program parameter). *)
| Unbounded of int (** only the lower bound is known,
there is no upper bound *)
+ | Unknown (** completely unknown relation. *)
module Range: Datatype.S_with_collections with type t = range
--
GitLab