[aorai] do not propagate \result as a binding to caller functions...

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

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;

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

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