[Interpreted automata] Add a dataflow computation functor

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
+

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
+

tests/misc/interpreted_automata_dataflow.i

+/* 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;
+}
+

tests/misc/interpreted_automata_dataflow.ml

+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

tests/misc/oracle/interpreted_automata_dataflow.res.oracle

+[kernel] Parsing tests/misc/interpreted_automata_dataflow.i (no preprocessing)
+[kernel] Results at the end of function main:
+  x -> 3
+  y -> 6
+  z -> 7