diff --git a/Changelog b/Changelog
index 84539e2642041d41ef960c7110ad5461f5785414..a358a708a6f498d4479cc58bbf0a17646eb89f3d 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,8 @@
Open Source Release <next-release>
##################################
+- Ivette [2022-10-26] After an Eva analysis with taint, the taint status of
+ lvalues is shown in the Inspector component and in Dive graphs.
- Eva [2022-10-25] The octagon domain can infer relations on the integer
conversion of floating-point variables.
- Ivette [2022-10-20] The installation of Frama-C provides an installation
@@ -32,8 +34,6 @@ o! From [2022-10-13] Removed Db.From API: use the From API instead.
- Kernel [2022-10-05] Support for ghost VLA and calls to builtins with
ghost arguments.
- Kernel [2022-10-03] -version prints a newline, -print-version does not.
-- Ivette [2022-09-30] After a taint Eva analysis, the taint status of
- lvalues and expressions is shown in the Inspector component.
- Eva [2022-09-16] Numerors now needs MLMPFR 4.1.0+bugfix2
o! Eva [2022-09-07] Deprecate Db.Value API: use the new Eva API instead.
- Kernel [2022-09-07] Improve error message for invalid options -D/-I/-U.
diff --git a/ivette/src/frama-c/kernel/Properties.tsx b/ivette/src/frama-c/kernel/Properties.tsx
index 992743ff4c890b8cce406f532cc797df62d110dc..f07eae5f7fa03286bf7048305a479b442c5b5cf8 100644
--- a/ivette/src/frama-c/kernel/Properties.tsx
+++ b/ivette/src/frama-c/kernel/Properties.tsx
@@ -262,8 +262,8 @@ const renderTaint: Renderer<States.Tag> =
let color = 'black';
switch (taint.name) {
case 'not_tainted': id = 'DROP.EMPTY'; color = '#00B900'; break;
- case 'data_tainted': id = 'DROP.FILLED'; color = '#FF8300'; break;
- case 'control_tainted': id = 'DROP.FILLED'; color = '#73BBBB'; break;
+ case 'direct_taint': id = 'DROP.FILLED'; color = '#882288'; break;
+ case 'indirect_taint': id = 'DROP.FILLED'; color = '#73BBBB'; break;
case 'error': id = 'HELP'; break;
case 'not_applicable': id = 'MINUS'; break;
default:
@@ -304,8 +304,8 @@ const byStatus =
const byTaint =
Compare.option(
Compare.byRank(
- 'data_tainted',
- 'control_tainted',
+ 'direct_taint',
+ 'indirect_taint',
'not_tainted',
'error',
'not_applicable',
diff --git a/ivette/src/frama-c/plugins/dive/api/index.ts b/ivette/src/frama-c/plugins/dive/api/index.ts
index d32321218879eb828e395b56c44940c0a874c99a..5f76720db27b2b6b30cceea094dba8f2127e988d 100644
--- a/ivette/src/frama-c/plugins/dive/api/index.ts
+++ b/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 */
diff --git a/ivette/src/frama-c/plugins/dive/style.json b/ivette/src/frama-c/plugins/dive/style.json
index 84d6611dee4a6c681a1a60f10845117e700dbbcd..ff9498762f52fa09bf66fe501ee44c427029e7a6 100644
--- a/ivette/src/frama-c/plugins/dive/style.json
+++ b/ivette/src/frama-c/plugins/dive/style.json
@@ -45,47 +45,57 @@
"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": ".function",
+ "selector": ":selected",
+ "style": {
+ "overlay-color": "#8bf",
+ "overlay-padding": "8px",
+ "overlay-opacity": 0.4
+ }
+ },
+ {
+ "selector": ".function, .file",
"style": {
"shape": "rectangle",
- "background-color": "#bbb",
+ "text-outline-width": 1,
+ "font-size": "11px",
"background-opacity" : 0.4,
"text-valign" : "top",
"text-halign" : "center",
- "padding" : "10px",
+ "padding" : "18px",
"border-width": 1
}
},
+ {
+ "selector": ".function",
+ "style": {
+ "background-color": "#bbb"
+ }
+ },
{
"selector": ".file",
"style": {
- "shape": "rectangle",
- "background-color": "#ddd",
- "background-opacity" : 0.4,
- "text-valign" : "top",
- "text-halign" : "center",
- "padding" : "10px",
- "border-width": 1
+ "background-color": "#ddd"
}
},
{
@@ -132,6 +142,15 @@
"background-color": "#e44"
}
},
+ {
+ "selector": "node[kind='const']",
+ "style": {
+ "shape": "ellipse",
+ "background-color": "#bbb",
+ "border-width": "1px",
+ "border-style": "dashed"
+ }
+ },
{
"selector": "node[kind='alarm']",
"style": {
@@ -155,6 +174,22 @@
"ghost-opacity": "0.7"
}
},
+ {
+ "selector": "node[taint='direct']",
+ "style": {
+ "underlay-color": "#882288",
+ "underlay-padding": "14px",
+ "underlay-opacity": 0.4
+ }
+ },
+ {
+ "selector": "node[taint='indirect']",
+ "style": {
+ "underlay-color": "#73BBBB",
+ "underlay-padding": "14px",
+ "underlay-opacity": 0.8
+ }
+ },
{
"selector": "edge[kind='callee']",
"style": {
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 22a877074d1b85d95b6d5e135cdf27a14d30292a..b34ea6c7b08ee0ee7edea5c72b8d65c53794ad34 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -87,12 +87,18 @@ module Eval =
struct
open Eva.Results
+ let at_start_of = at_start_of
+ let after = after
+ let after_kinstr = function
+ | Kglobal -> at_start (* After global initialization *)
+ | Kstmt stmt -> after stmt
+
let to_kf_list kinstr callee =
before_kinstr kinstr |> eval_callee callee |>
Result.value ~default:[]
- let to_cvalue kinstr lval =
- before_kinstr kinstr |> eval_lval lval |> as_cvalue
+ let to_cvalue request lval =
+ eval_lval lval request |> as_cvalue
let to_location kinstr lval =
before_kinstr kinstr |> eval_address lval |> as_location
@@ -103,6 +109,10 @@ struct
let to_callstacks stmt =
before stmt |> callstacks
+ let is_tainted request lval =
+ let zone = eval_address lval request |> as_zone in
+ is_tainted zone request |> Result.to_option
+
let studia_direct_effect = function
| e, { Studia.Writes.direct = true } -> Some e
| _ -> None
@@ -137,10 +147,15 @@ end
(* --- Precision evaluation --- *)
-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
+(* For folded bases, lval may be strictly included in the node zone *)
+let update_node_values node ?(lval=Node_kind.to_lval node.node_kind) rq =
+ match lval with
+ | None -> () (* can't evaluate node *)
+ | Some lval ->
+ let typ = Cil.typeOfLval lval
+ and cvalue = Eval.to_cvalue rq lval
+ and taint = Eval.is_tainted rq lval in
+ Graph.update_node_values node ~typ ~cvalue ~taint
(* --- Locations handling --- *)
@@ -226,7 +241,9 @@ let build_node_locality callstack node_kind =
let find_compatible_callstacks stmt callstack =
let kf = Kernel_function.find_englobing_kf stmt in
- if callstack <> [] && Kernel_function.equal kf (Callstack.top_kf callstack)
+ if callstack = [] (* Globals variables *)
+ then [Callstack.init kf] (* Default *)
+ else if Kernel_function.equal kf (Callstack.top_kf callstack)
then
(* slight improvement which only work when there is no recursion
and which is only usefull because you currently can't have
@@ -237,7 +254,12 @@ let find_compatible_callstacks stmt callstack =
(* Keep only callstacks which are a compatible with the current one *)
let callstacks = Eval.to_callstacks stmt in
(* TODO: missing callstacks filtered by memexec *)
- Callstack.filter_truncate callstacks callstack
+ let make_compatible cs =
+ Callstack.truncate_to_sub cs callstack |>
+ Option.value ~default:(Callstack.init kf)
+ in
+ let result = List.map make_compatible callstacks in
+ List.sort_uniq Callstack.compare result (* Remove duplicates *)
(* --- Graph building --- *)
@@ -257,9 +279,12 @@ let build_var context callstack varinfo =
let build_lval context callstack kinstr lval =
let node = build_node context callstack lval kinstr in
- update_node_values node kinstr lval;
+ update_node_values ~lval:(Some lval) node (Eval.after_kinstr kinstr);
node
+let build_const context callstack exp =
+ add_or_update_node context callstack (Const exp)
+
let build_alarm context callstack stmt alarm =
let node_kind = Alarm (stmt,alarm) in
let node_locality = build_node_locality callstack node_kind in
@@ -277,21 +302,25 @@ let build_node_writes context node =
let rec build_write_deps callstack kinstr lval : deps_builder =
let add_deps = function
| { skind=Instr instr } as stmt ->
+ (* Update the values at the light of new discovered write *)
+ update_node_values node (Eval.after stmt);
+ (* Add dependencies for each callstack *)
List.to_seq (find_compatible_callstacks stmt callstack) |>
Seq.flat_map (fun cs -> build_instr_deps cs stmt instr)
| _ -> assert false (* Studia invariant *)
in
let writes = Eval.writes kinstr lval in
- let args_seq, callee_stmts = build_arg_deps callstack in
+ let args_seq, call_stmts = build_arg_deps callstack in
let compare = Cil_datatype.Stmt_Id.compare in
- node.node_writes_stmts <- List.sort_uniq compare (writes @ callee_stmts);
+ node.node_writes_stmts <- List.sort_uniq compare (writes @ call_stmts);
Seq.append args_seq (Seq.flat_map add_deps (List.to_seq writes))
and build_alarm_deps callstack stmt alarm : deps_builder =
- List.to_seq (EnumLvals.in_alarm alarm) |>
- Seq.flat_map (build_lval_deps callstack stmt Data)
+ build_lvals_deps callstack stmt Data (EnumLvals.in_alarm alarm)
- and build_instr_deps callstack stmt : Cil_types.instr -> deps_builder = function
+ and build_instr_deps callstack stmt instr : deps_builder =
+ (* Add dependencies found in the instruction *)
+ match instr with
| Set (_, exp, _) ->
build_exp_deps callstack stmt Data exp
| Call (_, callee, args, _) ->
@@ -302,8 +331,13 @@ let build_node_writes context node =
in
Cil.treat_constructor_as_func as_func dest f args k loc
| Local_init (vi, AssignInit init, _) ->
- List.to_seq (EnumLvals.in_init vi init) |>
- Seq.flat_map (build_lval_deps callstack stmt Data)
+ let lvals = EnumLvals.in_init vi init in
+ let exp =
+ match init with
+ | CompoundInit _ -> None (* Do not generate nodes for Compounds for now *)
+ | SingleInit exp -> Some exp
+ in
+ build_lvals_deps callstack stmt Data ?exp lvals
| Asm _ | Skip _ | Code_annot _ -> Seq.empty (* Cases not returned by Studia *)
and build_arg_deps callstack : deps_builder * stmt list =
@@ -330,6 +364,8 @@ let build_node_writes context node =
| _ ->
assert false (* Callsites can only be Call or ConsInit *)
in
+ (* Evaluate the parameter values at the start of its defining function *)
+ update_node_values node (Eval.at_start_of kf);
Seq.flat_map add_deps (List.to_seq callsites), List.map fst callsites
| _ -> Seq.empty, []
@@ -362,21 +398,31 @@ let build_node_writes context node =
Seq.append callee_deps return_deps
and build_exp_deps callstack stmt kind exp : deps_builder =
- List.to_seq (EnumLvals.in_exp exp) |>
- Seq.flat_map (build_lval_deps callstack stmt kind)
+ let lvals = EnumLvals.in_exp exp in
+ build_lvals_deps callstack stmt kind ~exp lvals
+
+ and build_lvals_deps callstack stmt kind ?exp lvals : deps_builder =
+ if lvals <> [] then
+ List.to_seq lvals |>
+ Seq.flat_map (build_lval_deps callstack stmt kind)
+ else
+ Option.fold exp ~none:Seq.empty
+ ~some:(build_const_deps callstack stmt kind)
and build_lval_deps callstack stmt kind lval : deps_builder =
let kinstr = Kstmt stmt in
let dst = build_lval context callstack kinstr lval in
Seq.return (Graph.create_dependency graph kinstr dst kind node)
+ and build_const_deps callstack stmt kind exp : deps_builder =
+ let kinstr = Kstmt stmt in
+ let dst = build_const context callstack exp in
+ Seq.return (Graph.create_dependency graph kinstr dst kind node)
+
and build_scattered_deps callstack kinstr lval : deps_builder =
let add_cell node_kind =
let node' = add_or_update_node context callstack node_kind in
- begin match Node_kind.to_lval node_kind with
- | Some lval' -> update_node_values node kinstr lval';
- | _ -> ()
- end;
+ update_node_values node (Eval.after_kinstr kinstr);
Graph.create_dependency graph kinstr node' Composition node
in
enumerate_cells ~is_folded_base lval kinstr |> Seq.map add_cell
@@ -392,7 +438,7 @@ let build_node_writes context node =
build_scattered_deps callstack kinstr lval
| Alarm (stmt,alarm) ->
build_alarm_deps callstack stmt alarm
- | Unknown _ | AbsoluteMemory | String _ | Error _ ->
+ | Unknown _ | AbsoluteMemory | String _ | Const _ | Error _ ->
Seq.empty
@@ -507,7 +553,7 @@ let build_node_reads context node =
build_reads_deps callstack Kglobal (Cil_types.Var vi, Cil_types.NoOffset)
| Scattered (_lval,kinstr) ->
build_kinstr_deps callstack None kinstr
- | Alarm _ | Unknown _ | AbsoluteMemory | String _ | Error _ ->
+ | Alarm _ | Unknown _ | AbsoluteMemory | Const _ | String _ | Error _ ->
Seq.empty
diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml
index 3c5f769d4ce859af381b85af1017e0ff7566bd52..91959b12feb7d360f22f2e273cf0ce2868bfd39c 100644
--- a/src/plugins/dive/callstack.ml
+++ b/src/plugins/dive/callstack.ml
@@ -69,18 +69,7 @@ let truncate_to_sub full_cs sub_cs =
| [] -> None
| (s :: t) as cs ->
if is_prefix sub_cs cs
- then Some (List.rev acc @ sub_cs)
+ then Some (List.rev_append acc sub_cs)
else aux (s :: acc) t
in
aux [] full_cs
-
-let list_filter_map f l =
- let aux acc x =
- match f x with
- | None -> acc
- | Some y -> y :: acc
- in
- List.rev (List.fold_left aux [] l)
-
-let filter_truncate l sub_cs =
- list_filter_map (fun cs -> truncate_to_sub cs sub_cs) l
diff --git a/src/plugins/dive/callstack.mli b/src/plugins/dive/callstack.mli
index 68e2ded40c5251a6aee18e5d312eedb08f4f25ef..f179281b11f23d79955f916463366cc05c9e7b56 100644
--- a/src/plugins/dive/callstack.mli
+++ b/src/plugins/dive/callstack.mli
@@ -35,6 +35,13 @@ val pop : t -> (Cil_types.kernel_function * Cil_types.stmt * t) option
val pop_downto : Cil_types.kernel_function -> t -> t
val top_kf : t -> Cil_types.kernel_function
val push : Cil_types.kernel_function * Cil_types.stmt -> t -> t
+
+(* Dive use partial callstack where the first call in the callstack are
+ abstracted away. Thus, Dive callstack are prefixes of complete callstacks. *)
+
+(* [is_prefix sub full] returns true whenever [sub] is a prefix of [full] *)
val is_prefix : t -> t -> bool
+
+(* [truncate_to_sub full sub] removes [full] tail until [sub] becomes a suffix.
+ Returns None if [sub] is not included in [full] *)
val truncate_to_sub : t -> t -> t option
-val filter_truncate : t list -> t -> t list
diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml
index 736d4eb7df4977cc4acc74863add651286e3d155..297e16a2b8c6153cb3a104b3f9f690cd82912f53 100644
--- a/src/plugins/dive/dive_graph.ml
+++ b/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
@@ -223,6 +233,7 @@ let ouptput_to_dot out_channel g =
`Style `Bold ; `Color 0xff0000 ;
`Style `Filled ; `Fillcolor 0xff0000 ]
| AbsoluteMemory | String _ -> [`Shape `Box3d]
+ | Const _ -> [`Shape `Ellipse]
| Error _ -> [`Color 0xff0000]
and range = match v.node_range with
| Empty -> []
@@ -285,6 +296,7 @@ struct
| Alarm _ -> "alarm"
| AbsoluteMemory -> "absolute"
| String _ -> "string"
+ | Const _ -> "const"
| Error _ -> "error"
in
`String s
@@ -325,6 +337,11 @@ struct
| Partial _ -> `String "partial"
| NotDone -> `String "no"
+ let output_taint = function
+ | Eva.Results.Direct -> `String "direct"
+ | Indirect -> `String "indirect"
+ | Untainted -> `String "untainted"
+
let output_node node =
let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
`Assoc ([
@@ -345,6 +362,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) =
diff --git a/src/plugins/dive/dive_graph.mli b/src/plugins/dive/dive_graph.mli
index e2991d9b23bfd376d2d6f14b3b91085ecbebbcbe..48047ba03969f9ece36b0b3df814831fdffa7aaf 100644
--- a/src/plugins/dive/dive_graph.mli
+++ b/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
diff --git a/src/plugins/dive/dive_types.ml b/src/plugins/dive/dive_types.ml
index 56a623226171794d9aa9e00bf4318d98e70c407e..744900c6ee9a408392be96abcc93644e0d1ea526 100644
--- a/src/plugins/dive/dive_types.ml
+++ b/src/plugins/dive/dive_types.ml
@@ -28,6 +28,7 @@ type node_kind =
| Alarm of Cil_types.stmt * Alarms.alarm
| AbsoluteMemory
| String of int * Base.cstring
+ | Const of Cil_types.exp
| Error of string
type callstack = Callstack.t
@@ -53,6 +54,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;
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index 40e5bedeaf8f872607b942d83113d4e6bc718a2f..bbec83b346e9b6173d46353ef8cfc46f261114ef 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -70,6 +70,10 @@ struct
Datatype.Int.compare i1 i2
| String _, _ -> 1
| _, String _ -> -1
+ | Const e1, Const e2 ->
+ Cil_datatype.Exp.compare e1 e2
+ | Const _, _ -> 1
+ | _, Const _ -> -1
| Error s1, Error s2 ->
Datatype.String.compare s1 s2
@@ -86,6 +90,7 @@ struct
Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
| AbsoluteMemory, AbsoluteMemory -> true
| String (i,_), String (j,_) -> Datatype.Int.equal i j
+ | Const e1, Const e2 -> Cil_datatype.Exp.equal e1 e2
| Error s1, Error s2 -> Datatype.String.equal s1 s2
| _ -> false
@@ -102,7 +107,8 @@ struct
Hashtbl.hash (5, Stmt.hash stmt, Alarms.hash alarm)
| AbsoluteMemory -> 6
| String (i, _) -> Hashtbl.hash (7, i)
- | Error s -> Hashtbl.hash (8, s)
+ | Const e -> Hashtbl.hash (8, Cil_datatype.Exp.hash e)
+ | Error s -> Hashtbl.hash (9, s)
end
include Datatype.Make (DatatypeInput)
@@ -110,15 +116,15 @@ include Datatype.Make (DatatypeInput)
let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
- | Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory | String _ | Error _ ->
- None
+ | Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory
+ | String _ | Const _ | Error _ -> None
let to_lval = function
| Scalar (vi,_typ,offset) -> Some (Cil_types.Var vi, offset)
| Composite (vi) -> Some (Cil_types.Var vi, Cil_types.NoOffset)
| Scattered (lval,_) -> Some lval
| Unknown (lval,_) -> Some lval
- | Alarm (_,_) | AbsoluteMemory | String _ | Error _ -> None
+ | Alarm (_,_) | AbsoluteMemory | String _ | Const _ | Error _ -> None
let pretty fmt = function
| (Scalar _ | Composite _ | Scattered _ | Unknown _) as kind ->
@@ -131,5 +137,7 @@ let pretty fmt = function
Format.fprintf fmt "%S" s
| String (_, CSWstring s) ->
Format.fprintf fmt "L\"%s\"" (Escape.escape_wstring s)
+ | Const e ->
+ Format.fprintf fmt "%a" Cil_printer.pp_exp e
| Error s ->
Format.fprintf fmt "%s" s
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 7f8cd7e4177a5a80402c8001e6b22c2e68231eaa..c29359d807dfe9b61e29856dd20a0ef6cd89ce80 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/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
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
index 198c8cfc1b73565cfe4d1c33cf09e0f2dfc30938..a1190d2d94fd0e19e93369c4f7543bcf51d966d6 100644
--- a/src/plugins/dive/tests/dive/oracle/assigned_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<w>, shape=box, style="bold", ];
+ cp2 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_global.dot b/src/plugins/dive/tests/dive/oracle/callstack_global.dot
index 620122edbd9a85a3fb5d89aa19bd43adf4209815..d2245d10a588309fb482b7056f5153ce5016c37c 100644
--- a/src/plugins/dive/tests/dive/oracle/callstack_global.dot
+++ b/src/plugins/dive/tests/dive/oracle/callstack_global.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<r>, shape=box, style="bold", ];
+ cp2 [label=<r>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled,bold", ];
cp3 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
cp5 [label=<tmp_0>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
@@ -16,8 +17,10 @@ digraph G {
style="filled", ];
cp19 [label=<x1>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
+ cp21 [label=<39>, shape=ellipse, ];
+ cp23 [label=<3>, shape=ellipse, ];
- subgraph cluster_cs_1 { label=<main>; cp19;cp17;cp5;cp3;cp2;
+ subgraph cluster_cs_1 { label=<main>; cp23;cp21;cp19;cp17;cp5;cp3;cp2;
subgraph cluster_cs_2 { label=<f>; cp7;
};
subgraph cluster_cs_3 { label=<f>; cp9;
@@ -38,5 +41,7 @@ digraph G {
cp15 -> cp11;
cp17 -> cp15;
cp19 -> cp15;
+ cp21 -> cp17;
+ cp23 -> cp19;
}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
index 0ef329150cf7afe934680a761cb96bb07b9429ea..1944fac8cbf2e0aeb6d60f86d28a5cb43919f25e 100644
--- a/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
+++ b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<r>, shape=box, style="bold", ];
+ cp2 [label=<r>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/const.dot b/src/plugins/dive/tests/dive/oracle/const.dot
index 6ea580760fe17d262fd3be8c9f9c039e10fe7b26..bb67ee0a8f13e3ffdc2fa6069374d215300f5673 100644
--- a/src/plugins/dive/tests/dive/oracle/const.dot
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<res>, shape=box, style="bold", ];
+ cp2 [label=<res>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<__retres>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<c>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.dot b/src/plugins/dive/tests/dive/oracle/exceptional.dot
index a512210f1c4dadb0f008955da870206c6de2c373..b2e11483ced54ea2c35fe6c937654d0f7e265213 100644
--- a/src/plugins/dive/tests/dive/oracle/exceptional.dot
+++ b/src/plugins/dive/tests/dive/oracle/exceptional.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<__retres>, shape=box, style="bold", ];
+ cp2 [label=<__retres>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<a>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/global.dot b/src/plugins/dive/tests/dive/oracle/global.dot
index de476dbaf1ee931794d2fb600ed7bc857b708e9f..36c6ca1aa9f8d8457b593fa6eccfe780127a22bc 100644
--- a/src/plugins/dive/tests/dive/oracle/global.dot
+++ b/src/plugins/dive/tests/dive/oracle/global.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<z>, shape=box, style="bold", ];
+ cp2 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<g>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/manydeps.dot b/src/plugins/dive/tests/dive/oracle/manydeps.dot
index bcffeba804e729b864d5f0dfae03c06f4e6adf63..d00972c3173b5d36ee80a6ec993194f0333bc635 100644
--- a/src/plugins/dive/tests/dive/oracle/manydeps.dot
+++ b/src/plugins/dive/tests/dive/oracle/manydeps.dot
@@ -11,13 +11,20 @@ digraph G {
style="filled", ];
cp12 [label=<t10>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp14 [label=<__retres>, shape=box, style="bold", ];
- cp15 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
+ cp14 [label=<0>, shape=ellipse, ];
+ cp16 [label=<0>, shape=ellipse, ];
+ cp18 [label=<0>, shape=ellipse, ];
+ cp20 [label=<0>, shape=ellipse, ];
+ cp22 [label=<0>, shape=ellipse, ];
+ cp24 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled,bold", ];
+ cp25 [label=<0>, shape=ellipse, ];
+ cp27 [label=<*(pt[x])>, shape=parallelogram, fillcolor="#AACCFF",
color="#88AAFF", style="filled,dotted", ];
- subgraph cluster_cs_1 { label=<many_writes>; cp12;cp10;cp8;cp6;cp4;cp2;
+ subgraph cluster_cs_1 { label=<many_writes>; cp22;cp20;cp18;cp16;cp14;cp12;cp10;cp8;cp6;cp4;cp2;
};
- subgraph cluster_cs_2 { label=<many_values>; cp15;cp14;
+ subgraph cluster_cs_2 { label=<many_values>; cp27;cp25;cp24;
};
cp2 -> cp2 [style="bold", ];
@@ -26,6 +33,12 @@ digraph G {
cp8 -> cp2;
cp10 -> cp2;
cp12 -> cp2;
- cp15 -> cp14;
+ cp14 -> cp4;
+ cp16 -> cp6;
+ cp18 -> cp8;
+ cp20 -> cp10;
+ cp22 -> cp12;
+ cp25 -> cp24 [style="bold", ];
+ cp27 -> cp24;
}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/per_callstack.dot b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
index 22fa39f4a0bafda9b87dbf7e3f399ab452d241f3..0ae6f71c8c46c41651bae04ccc5c34b62cc54fc1 100644
--- a/src/plugins/dive/tests/dive/oracle/per_callstack.dot
+++ b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<w>, shape=box, style="bold", ];
+ cp2 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/pointed_param.dot b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
index f2713a435f62e45b60876cd9ad143d53675ead1b..92f573361740169815209ed17afccd6a326b8974 100644
--- a/src/plugins/dive/tests/dive/oracle/pointed_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<y>, shape=box, style="bold", ];
+ cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot b/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot
index 243f81deb0cb5a035debce97194e9b1a338f41d3..b7876f50b929e04fe0f2704a4debfca7d0d72e98 100644
--- a/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot
+++ b/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot
@@ -1,20 +1,22 @@
digraph G {
cp2 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled,bold", ];
- cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ cp3 [label=<0.0f>, shape=ellipse, ];
+ cp5 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp6 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ cp8 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- subgraph cluster_cs_1 { label=<main>; cp2;
- subgraph cluster_cs_4 { label=<f2>; cp6;
+ subgraph cluster_cs_1 { label=<main>; cp3;cp2;
+ subgraph cluster_cs_4 { label=<f2>; cp8;
};
};
cp2 -> cp2;
- cp2 -> cp3;
- cp2 -> cp6;
+ cp2 -> cp5;
+ cp2 -> cp8;
cp3 -> cp2;
- cp6 -> cp2;
+ cp5 -> cp2;
+ cp8 -> cp2;
}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/ranges.dot b/src/plugins/dive/tests/dive/oracle/ranges.dot
index c6e74f511d0dcd51b0654f7e0c8fb395464ba343..6c5989ea7f6c318bd227bd79f1caa8d57a1fce94 100644
--- a/src/plugins/dive/tests/dive/oracle/ranges.dot
+++ b/src/plugins/dive/tests/dive/oracle/ranges.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<res>, shape=box, style="bold", ];
+ cp2 [label=<res>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<i>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<f>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
@@ -36,8 +37,38 @@ digraph G {
style="filled", ];
cp37 [label=<f7>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
+ cp39 [label=<2>, shape=ellipse, ];
+ cp41 [label=<0>, shape=ellipse, ];
+ cp43 [label=<3>, shape=ellipse, ];
+ cp45 [label=<0>, shape=ellipse, ];
+ cp47 [label=<12>, shape=ellipse, ];
+ cp49 [label=<0>, shape=ellipse, ];
+ cp51 [label=<127>, shape=ellipse, ];
+ cp53 [label=<0>, shape=ellipse, ];
+ cp55 [label=<42000>, shape=ellipse, ];
+ cp57 [label=<0>, shape=ellipse, ];
+ cp59 [label=<1350000>, shape=ellipse, ];
+ cp61 [label=<0>, shape=ellipse, ];
+ cp63 [label=<910000000>, shape=ellipse, ];
+ cp65 [label=<0>, shape=ellipse, ];
+ cp67 [label=<2000000000>, shape=ellipse, ];
+ cp69 [label=<(float)0.>, shape=ellipse, ];
+ cp71 [label=<0.f>, shape=ellipse, ];
+ cp73 [label=<0.001f>, shape=ellipse, ];
+ cp75 [label=<0.f>, shape=ellipse, ];
+ cp77 [label=<3.14f>, shape=ellipse, ];
+ cp79 [label=<0.f>, shape=ellipse, ];
+ cp81 [label=<1020.f>, shape=ellipse, ];
+ cp83 [label=<0.f>, shape=ellipse, ];
+ cp85 [label=<1e7f>, shape=ellipse, ];
+ cp87 [label=<0.f>, shape=ellipse, ];
+ cp89 [label=<1e20f>, shape=ellipse, ];
+ cp91 [label=<0.f>, shape=ellipse, ];
+ cp93 [label=<1e36f>, shape=ellipse, ];
+ cp95 [label=<0.f>, shape=ellipse, ];
+ cp97 [label=<1e37f>, shape=ellipse, ];
- subgraph cluster_cs_1 { label=<main>; cp37;cp35;cp33;cp31;cp29;cp27;cp25;cp23;cp21;cp19;cp17;cp15;cp13;cp11;cp9;cp7;cp5;cp3;cp2;
+ subgraph cluster_cs_1 { label=<main>; cp97;cp95;cp93;cp91;cp89;cp87;cp85;cp83;cp81;cp79;cp77;cp75;cp73;cp71;cp69;cp67;cp65;cp63;cp61;cp59;cp57;cp55;cp53;cp51;cp49;cp47;cp45;cp43;cp41;cp39;cp37;cp35;cp33;cp31;cp29;cp27;cp25;cp23;cp21;cp19;cp17;cp15;cp13;cp11;cp9;cp7;cp5;cp3;cp2;
};
cp3 -> cp2;
@@ -58,5 +89,35 @@ digraph G {
cp33 -> cp5;
cp35 -> cp5;
cp37 -> cp5;
+ cp39 -> cp7;
+ cp41 -> cp9;
+ cp43 -> cp9;
+ cp45 -> cp11;
+ cp47 -> cp11;
+ cp49 -> cp13;
+ cp51 -> cp13;
+ cp53 -> cp15;
+ cp55 -> cp15;
+ cp57 -> cp17;
+ cp59 -> cp17;
+ cp61 -> cp19;
+ cp63 -> cp19;
+ cp65 -> cp21;
+ cp67 -> cp21;
+ cp69 -> cp23;
+ cp71 -> cp25;
+ cp73 -> cp25;
+ cp75 -> cp27;
+ cp77 -> cp27;
+ cp79 -> cp29;
+ cp81 -> cp29;
+ cp83 -> cp31;
+ cp85 -> cp31;
+ cp87 -> cp33;
+ cp89 -> cp33;
+ cp91 -> cp35;
+ cp93 -> cp35;
+ cp95 -> cp37;
+ cp97 -> cp37;
}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot b/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
index a76ec08dcb670c953f4f2e4e2903ed78d0a5f724..1978773631238f75819acf83686dc50b242d2366 100644
--- a/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
+++ b/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
@@ -1,5 +1,6 @@
digraph G {
- cp2 [label=<x>, shape=box, style="bold", ];
+ cp2 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index 26e624b56755b7493ae275b0e264119d8c75867d..d661acee21a6b81d2dc2e4e1243d9adafee1eee7 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -7,7 +7,8 @@ digraph G {
style="filled", ];
cp8 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp11 [label=<z>, shape=box, style="bold", ];
+ cp11 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,bold", ];
cp12 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
cp14 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
@@ -22,21 +23,22 @@ digraph G {
style="filled", ];
cp25 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
- cp29 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ cp28 [label=<& f>, shape=ellipse, ];
+ cp31 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
- cp32 [label=<is_nan_or_infinite: \is_finite((float)\mul_double((double)y, (double)2.0))>,
+ cp34 [label=<is_nan_or_infinite: \is_finite((float)\mul_double((double)y, (double)2.0))>,
fillcolor="#FF0000", color="#FF0000", shape=doubleoctagon,
style="filled,bold,bold", ];
- cp34 [label=<is_nan_or_infinite: \is_finite(\add_float(y, w))>,
+ cp36 [label=<is_nan_or_infinite: \is_finite(\add_float(y, w))>,
fillcolor="#FF0000", color="#FF0000", shape=doubleoctagon,
style="filled,bold,bold", ];
- subgraph cluster_cs_1 { label=<f>; cp32;cp5;cp2;
+ subgraph cluster_cs_1 { label=<f>; cp34;cp5;cp2;
};
- subgraph cluster_cs_2 { label=<main>; cp34;cp23;cp18;cp14;cp12;cp11;cp3;
+ subgraph cluster_cs_2 { label=<main>; cp36;cp28;cp23;cp18;cp14;cp12;cp11;cp3;
subgraph cluster_cs_3 { label=<f>; cp21;cp16;
};
- subgraph cluster_cs_4 { label=<f>; cp29;cp25;
+ subgraph cluster_cs_4 { label=<f>; cp31;cp25;
};
};
subgraph cluster_file_1 { label=<various.i>; cp8;
@@ -48,19 +50,20 @@ digraph G {
cp3 -> cp16;
cp3 -> cp25;
cp5 -> cp2;
- cp5 -> cp32;
+ cp5 -> cp34;
cp8 -> cp3;
cp12 -> cp11;
- cp12 -> cp34;
+ cp12 -> cp36;
cp14 -> cp11;
- cp14 -> cp34;
+ cp14 -> cp36;
cp16 -> cp12;
cp16 -> cp21;
cp18 -> cp14;
cp21 -> cp16;
cp23 -> cp18 [color="#00FF00", ];
cp25 -> cp18;
- cp25 -> cp29;
- cp29 -> cp25;
+ cp25 -> cp31;
+ cp28 -> cp23;
+ cp31 -> cp25;
}
\ No newline at end of file