[Dive] add taint information

ivette/src/frama-c/plugins/dive/api/index.ts

@@ -150,7 +150,7 @@ export type node =
   { id: nodeId, label: string, kind: string, locality: nodeLocality,
     is_root: boolean, backward_explored: string, forward_explored: string,
     writes: location[], values?: string, range: number | string,
-    type?: string };
+    type?: string, taint?: "direct" | "indirect" | "untainted" };
 
 /** Decoder for `node` */
 export const jNode: Json.Decoder<node> =
@@ -166,6 +166,12 @@ export const jNode: Json.Decoder<node> =
     values: Json.jOption(Json.jString),
     range: Json.jUnion<number | string>( Json.jNumber, Json.jString,),
     type: Json.jOption(Json.jString),
+    taint: Json.jOption(
+             Json.jUnion<"direct" | "indirect" | "untainted">(
+               Json.jTag("direct"),
+               Json.jTag("indirect"),
+               Json.jTag("untainted"),
+             )),
   });
 
 /** Natural order for `node` */
@@ -174,7 +180,7 @@ export const byNode: Compare.Order<node> =
     <{ id: nodeId, label: string, kind: string, locality: nodeLocality,
        is_root: boolean, backward_explored: string, forward_explored: string,
        writes: location[], values?: string, range: number | string,
-       type?: string }>({
+       type?: string, taint?: "direct" | "indirect" | "untainted" }>({
     id: byNodeId,
     label: Compare.string,
     kind: Compare.string,
@@ -186,6 +192,7 @@ export const byNode: Compare.Order<node> =
     values: Compare.defined(Compare.string),
     range: Compare.structural,
     type: Compare.defined(Compare.string),
+    taint: Compare.defined(Compare.structural),
   });
 
 /** The dependency between two nodes */

ivette/src/frama-c/plugins/dive/style.json

@@ -45,22 +45,31 @@
       "curve-style": "bezier",
       "target-arrow-shape": "vee",
       "target-arrow-color": "#888",
-      "arrow-scale": 2.0
+      "arrow-scale": 2.0,
+      "z-compound-depth": "top"
     }
   },
   {
     "selector": "edge.multiple-selection",
     "style": {
       "overlay-color": "#aaa",
-      "overlay-padding": "10px",
+      "overlay-padding": "4px",
       "overlay-opacity": 0.4
     }
   },
   {
-    "selector": "edge.selection, :selected",
+    "selector": "edge.selection",
     "style": {
       "overlay-color": "#8bf",
-      "overlay-padding": "10px",
+      "overlay-padding": "4px",
+      "overlay-opacity": 0.4
+    }
+  },
+  {
+    "selector": ":selected",
+    "style": {
+      "overlay-color": "#8bf",
+      "overlay-padding": "8px",
       "overlay-opacity": 0.4
     }
   },
@@ -155,6 +164,22 @@
       "ghost-opacity": "0.7"
     }
   },
+  {
+    "selector": "node[taint='direct']",
+    "style": {
+      "underlay-color": "#afa",
+      "underlay-padding": "14px",
+      "underlay-opacity": 1.0
+    }
+  },
+  {
+    "selector": "node[taint='indirect']",
+    "style": {
+      "underlay-color": "#afa",
+      "underlay-padding": "14px",
+      "underlay-opacity": 0.5
+    }
+  },
   {
     "selector": "edge[kind='callee']",
     "style": {

src/plugins/dive/build.ml

@@ -103,6 +103,10 @@ struct
   let to_callstacks stmt =
     before stmt |> callstacks
 
+  let is_tainted kinstr lval =
+    let zone = to_zone kinstr lval in
+    before_kinstr kinstr |> is_tainted zone |> Result.to_option
+
   let studia_direct_effect = function
     | e, { Studia.Writes.direct = true } -> Some e
     | _ -> None
@@ -139,8 +143,9 @@ end
 
 let update_node_values node kinstr lval =
   let typ = Cil.typeOfLval lval
-  and cvalue = Eval.to_cvalue kinstr lval in
-  Graph.update_node_values node cvalue typ
+  and cvalue = Eval.to_cvalue kinstr lval
+  and taint = Eval.is_tainted kinstr lval in
+  Graph.update_node_values node ~typ ~cvalue ~taint
 
 
 (* --- Locations handling --- *)

src/plugins/dive/dive_graph.ml

@@ -37,6 +37,7 @@ let new_node
   node_hidden = false;
   node_values = None;
   node_range = Empty;
+  node_taint = None;
   node_writes_computation = NotDone;
   node_reads_computation = NotDone;
   node_writes_stmts = [];
@@ -123,12 +124,21 @@ let edges g =
   fold_edges_e (fun d acc -> d ::acc) g []
 
 
-let update_node_values node new_values typ =
-  let join n = Cvalue.V.join n new_values in
-  node.node_values <-
-    Some (Option.fold ~some:join ~none:new_values node.node_values);
+let update_node_values node ~typ ~cvalue ~taint =
+  let join_taint t1 t2 =
+    let open Eva.Results in
+    match t1, t2 with
+    | Direct, _ | _, Direct -> Direct
+    | Indirect, _ | _, Indirect -> Indirect
+    | Untainted, Untainted -> Untainted
+  in
+  node.node_values <- Some (
+      Option.fold ~some:(Cvalue.V.join cvalue) ~none:cvalue node.node_values);
   node.node_range <-
-    Node_range.(upper_bound node.node_range (evaluate new_values typ))
+    Node_range.(upper_bound node.node_range (evaluate cvalue typ));
+  Option.iter (fun taint ->
+      node.node_taint <- Some (
+          Option.fold ~some:(join_taint taint) ~none:taint node.node_taint)) taint
 
 let find_independant_nodes g roots =
   let module Dfs = Graph.Traverse.Dfs (struct
@@ -325,6 +335,11 @@ struct
     | Partial _ -> `String "partial"
     | NotDone -> `String "no"
 
+  let output_taint = function
+    | Eva.Results.Direct -> `String "direct"
+    | Indirect ->  `String "inddirect"
+    | Untainted ->  `String "untainted"
+
   let output_node node =
     let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
     `Assoc ([
@@ -345,6 +360,10 @@ struct
             let typ = Cil.typeOfLval lval in
             let str = Pretty_utils.to_string Cil_printer.pp_typ typ in
             [("type", `String str)]
+        end @
+        begin match node.node_taint with
+          | None -> []
+          | Some t -> [("taint", output_taint t)]
         end)
 
   let output_dep (n1,dep,n2) =

src/plugins/dive/dive_graph.mli

@@ -38,7 +38,9 @@ val create_node :
 
 val remove_node : t -> node -> unit
 
-val update_node_values : node -> Cvalue.V.t -> Cil_types.typ -> unit
+val update_node_values : node ->
+  typ:Cil_types.typ -> cvalue:Cvalue.V.t -> taint:Eva.Results.taint option ->
+  unit
 
 val create_dependency : t -> Cil_types.kinstr ->
   node -> dependency_kind -> node -> unit

src/plugins/dive/dive_types.ml

@@ -53,6 +53,7 @@ type node = {
   mutable node_hidden : bool;
   mutable node_values : Cvalue.V.t option;
   mutable node_range : node_range;
+  mutable node_taint : Eva.Results.taint option;
   mutable node_writes_computation : computation;
   mutable node_reads_computation : computation;
   mutable node_writes_stmts : Cil_types.stmt list;

src/plugins/dive/server_interface.ml

@@ -200,7 +200,9 @@ struct
       "writes", Jarray Kernel_ast.KfMarker.jtype;
       "values", Joption Jstring;
       "range", Junion [ Jnumber ; Jstring ];
-      "type", Joption Jstring
+      "type", Joption Jstring;
+      "taint", Joption (Junion [
+          Jtag "direct"; Jtag "indirect"; Jtag "untainted"])
     ])
 end