From 6bc0ed2d2c9744b8be5e1d33ebb6d489cf0366fc Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 23 Apr 2019 19:11:45 +0200
Subject: [PATCH] [Interpreted automata] Add a dataflow computation functor
---
.../analysis/interpreted_automata.ml | 88 ++++++++++++++
.../analysis/interpreted_automata.mli | 18 +++
tests/misc/interpreted_automata_dataflow.i | 23 ++++
tests/misc/interpreted_automata_dataflow.ml | 115 ++++++++++++++++++
.../interpreted_automata_dataflow.res.oracle | 5 +
5 files changed, 249 insertions(+)
create mode 100644 tests/misc/interpreted_automata_dataflow.i
create mode 100644 tests/misc/interpreted_automata_dataflow.ml
create mode 100644 tests/misc/oracle/interpreted_automata_dataflow.res.oracle
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index fd73d9c1eb2..a1159e205a6 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -941,6 +941,9 @@ let is_wto_head kf = Compute.is_wto_head (get_wto_index_table kf)
let is_back_edge kf = Compute.is_back_edge (get_wto_index_table kf)
+(* ---------------------------------------------------------------------- *)
+(* --- Graph with only one entry per component --- *)
+(* ---------------------------------------------------------------------- *)
module UnrollUnnatural = struct
@@ -1090,3 +1093,88 @@ module UnrollUnnatural = struct
g'
end
+
+
+(* ---------------------------------------------------------------------- *)
+(* --- Dataflow computation --- *)
+(* ---------------------------------------------------------------------- *)
+
+module type Domain =
+sig
+ type t
+
+ val join : t -> t -> t
+ val widen : t -> t -> t option (* returns None when inclusion *)
+ val transfer : vertex transition -> t -> t option
+end
+
+
+module Dataflow (D : Domain) =
+struct
+ module Results = Vertex.Hashtbl
+
+ let fixpoint kf initial_value =
+ let automaton = get_automaton kf in
+ let graph = automaton.graph in
+ let wto = get_wto kf in
+ let results = Results.create (G.nb_vertex graph) in
+
+ (* Compute the transfer function for the given edge and add the result to
+ acc *)
+ let process_edge (v1,e,_v2) acc =
+ (* Retrieve origin value *)
+ match Results.find_opt results v1 with
+ | None -> acc (* No previous value *)
+ | Some value ->
+ match D.transfer e.edge_transition value with
+ | None -> acc
+ | Some new_value -> new_value :: acc
+ in
+
+ (* Compute the abstract value for the given control point ; compute all
+ incoming transfer functions *)
+ let process_vertex v =
+ let incomming = G.fold_pred_e process_edge graph v []
+ and initial = if v == automaton.entry_point then [initial_value] else []
+ in
+ match initial @ incomming with
+ | [] -> (* Zero incomming values -> Bottom *)
+ Results.remove results v
+ | v1 :: vl ->
+ (* Join incomming values *)
+ let result = List.fold_left D.join v1 vl in
+ Results.add results v result
+ in
+
+ (* widen returns whether it is necessary to continue to iterate or not *)
+ let widen v previous =
+ let current = Results.find_opt results v in
+ match previous, current with
+ | _, None -> false (* Current is bottom, let's quit *)
+ | None, _ -> true (* Previous was bottom *)
+ | Some v1, Some v2 ->
+ match D.widen v1 v2 with
+ | None -> false (* End of iteration *)
+ | Some value -> (* new value *)
+ Results.add results v value;
+ true
+ in
+
+ let rec iterate_list l =
+ List.iter iterate_element l
+ and iterate_element = function
+ | Wto.Node v ->
+ ignore (process_vertex v)
+ | Wto.Component (v, w) ->
+ while
+ let previous = Results.find_opt results v in
+ process_vertex v;
+ widen v previous
+ do
+ iterate_list w;
+ done;
+ in
+ iterate_list wto;
+ results
+end
+
diff --git a/src/kernel_services/analysis/interpreted_automata.mli b/src/kernel_services/analysis/interpreted_automata.mli
index c7c1b86d873..dec17586091 100644
--- a/src/kernel_services/analysis/interpreted_automata.mli
+++ b/src/kernel_services/analysis/interpreted_automata.mli
@@ -244,3 +244,21 @@ module UnrollUnnatural : sig
automaton -> wto -> Compute.wto_index_table -> G.t
end
+
+
+(* Dataflow computation *)
+
+module type Domain =
+sig
+ type t
+
+ val join : t -> t -> t
+ val widen : t -> t -> t option (* returns None when inclusion *)
+ val transfer : vertex transition -> t -> t option
+end
+
+module Dataflow (D : Domain) :
+sig
+ val fixpoint : Cil_types.kernel_function -> D.t -> D.t Vertex.Hashtbl.t
+end
+
diff --git a/tests/misc/interpreted_automata_dataflow.i b/tests/misc/interpreted_automata_dataflow.i
new file mode 100644
index 00000000000..0dbe0d14845
--- /dev/null
+++ b/tests/misc/interpreted_automata_dataflow.i
@@ -0,0 +1,23 @@
+/* run.config
+OPT: -load-script tests/misc/interpreted_automata_dataflow.ml
+*/
+
+void main(int x)
+{
+ int y = 3;
+ y = y * 2;
+
+ int z = y + 1;
+ int w = y + x;
+ int a = 1;
+
+ for (int i = 0 ; i < 10 ; i ++) {
+ int b = 3;
+ int c = i + 1;
+ a = a + 1;
+ }
+
+ if (x != 3)
+ x = 3;
+}
+
diff --git a/tests/misc/interpreted_automata_dataflow.ml b/tests/misc/interpreted_automata_dataflow.ml
new file mode 100644
index 00000000000..b23a0a3cd8d
--- /dev/null
+++ b/tests/misc/interpreted_automata_dataflow.ml
@@ -0,0 +1,115 @@
+open Cil_types
+
+module Map = Cil_datatype.Varinfo.Map
+
+module ConstantsDomain =
+struct
+ type t = int Map.t
+
+ let top = Map.empty
+
+ let pretty fmt v =
+ let pp_entry vi x =
+ Format.fprintf fmt "%s -> %d@." vi.vorig_name x
+ in
+ Map.iter pp_entry v
+
+ let join v1 v2 =
+ let merge_entry _vi o1 o2 =
+ match o1, o2 with
+ | None, _ | _, None -> None
+ | Some x, Some x' -> if x = x' then Some x else None
+ in
+ Map.merge merge_entry v1 v2
+
+ let widen v1 v2 =
+ let same_entry vi x =
+ Map.find_opt vi v2 = Some x
+ in
+ if Map.for_all same_entry v1 then
+ None (* Inclusion *)
+ else
+ Some v2 (* No widening necessary *)
+
+ exception Not_constant
+
+ let rec eval v exp =
+ match exp.enode with
+ | Const (CInt64 (i,_,_)) ->
+ (try Integer.to_int i with _ -> raise Not_constant)
+ | Lval (Var vi, NoOffset) ->
+ (try Map.find vi v with Not_found -> raise Not_constant)
+ | SizeOf typ ->
+ Cil.bytesSizeOf typ
+ | UnOp (Neg, e, _) ->
+ -(eval v e)
+ | BinOp (PlusA, e1, e2, _) ->
+ (eval v e1) + (eval v e2)
+ | BinOp (MinusA, e1, e2, _) ->
+ (eval v e1) - (eval v e2)
+ | BinOp (Mult, e1, e2, _) ->
+ (eval v e1) * (eval v e2)
+ | BinOp (Div, e1, e2, _) ->
+ let x = eval v e2 in
+ if x <> 0 then (eval v e1) / x else raise Not_constant
+ | _ ->
+ raise Not_constant
+
+ let eval_opt v exp =
+ try Some (eval v exp) with Not_constant -> None
+
+ let assume v exp kind =
+ match exp.enode, kind with
+ | BinOp (Eq, e1, e2, _), Interpreted_automata.Then
+ | BinOp (Ne, e1, e2, _), Interpreted_automata.Else ->
+ begin match eval_opt v e1, eval_opt v e2 with
+ | None, None -> Some v
+ | Some x, None ->
+ begin match e2.enode with
+ | Lval (Var vi, NoOffset) -> Some (Map.add vi x v)
+ | _ -> Some v
+ end
+ | None, Some x ->
+ begin match e1.enode with
+ | Lval (Var vi, NoOffset) -> Some (Map.add vi x v)
+ | _ -> Some v
+ end
+ | Some x, Some y ->
+ if x = y then Some v else None
+ end
+ | _ -> Some v
+
+ let assign v vi exp =
+ try
+ Map.add vi (eval v exp) v
+ with Not_constant ->
+ Map.remove vi v
+
+ let transfer t v =
+ let open Interpreted_automata in
+ match t with
+ | Skip | Return _ | Prop _ | Enter _ | Leave _ -> Some v
+ | Guard (exp, kind, _) -> assume v exp kind
+ | Instr (Set ((Var vi, NoOffset), exp, _), _) -> Some (assign v vi exp)
+ | Instr (Local_init (vi, AssignInit (SingleInit exp), _), _) ->
+ Some (assign v vi exp)
+ | Instr (Local_init (_vi, AssignInit (CompoundInit _), _), _) -> Some v
+ | Instr ((Call _ | Local_init _ | Set _ | Asm _), _) -> Some top
+ | Instr ((Cil_types.Skip _ | Code_annot _), _) -> Some v
+end
+
+
+module Dataflow = Interpreted_automata.Dataflow (ConstantsDomain)
+
+let run () =
+ let main_kf, _ = Globals.entry_point () in
+ let results = Dataflow.fixpoint main_kf ConstantsDomain.top in
+ let result = Interpreted_automata.(
+ Vertex.Hashtbl.find results (get_automaton main_kf).return_point)
+ in
+ Kernel.result "Results at the end of function %s:@.%a"
+ (Kernel_function.get_name main_kf)
+ ConstantsDomain.pretty result
+
+let () =
+ Db.Main.extend run
diff --git a/tests/misc/oracle/interpreted_automata_dataflow.res.oracle b/tests/misc/oracle/interpreted_automata_dataflow.res.oracle
new file mode 100644
index 00000000000..75741cada58
--- /dev/null
+++ b/tests/misc/oracle/interpreted_automata_dataflow.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing tests/misc/interpreted_automata_dataflow.i (no preprocessing)
+[kernel] Results at the end of function main:
+ x -> 3
+ y -> 6
+ z -> 7
--
GitLab