diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml index 11777c663fcfc899da9f6c1d2cebc1a1ddc0f92b..4463838589f4a0439ed9f8b870d4eeac81396dbb 100644 --- a/src/plugins/dive/build.ml +++ b/src/plugins/dive/build.ml @@ -157,54 +157,55 @@ let is_foldable_type typ = | TBuiltin_va_list _ -> false | TNamed _ -> assert false (* the type have been unrolled *) -exception NoMatchingOffset -let cell_to_scalar typ vi offset = - (* TODO: exceptions must be shown to the user somehow *) - try - let matching = Bit_utils.MatchType typ in - let offset', _ = Bit_utils.find_offset vi.vtype ~offset matching in - Scalar (vi, typ, offset') - with Bit_utils.NoMatchingOffset -> raise NoMatchingOffset - -exception NotACell exception Too_many_deps of node_kind list +exception Unknown_location let enumerate_cells ~is_folded_base ~limit lval kinstr = - (* TODO: non-variable bases must be shown to the user somehow *) (* If possible, refine the lval to a non-symbolic one *) - let location = !Db.Value.lval_to_loc kinstr lval - and typ = Cil.typeOfLval lval in + let typ = Cil.typeOfLval lval in + let state = Db.Value.get_state kinstr in + let location = !Db.Value.lval_to_loc_state state lval in let open Locations in let add (acc,count) node_kind = - if count > limit then + if count >= limit then raise (Too_many_deps acc); (node_kind :: acc, count+1) in let add_base base ival (acc,count) = match base with - | Base.Var (vi,_) -> + | Base.Var (vi,_) | Allocated (vi,_,_) -> begin if is_foldable_type vi.vtype && is_folded_base vi then add (acc,count) (Composite (vi)) else - let add_cells offset (acc,count) = - add (acc,count) (cell_to_scalar typ vi offset) + let add_cell offset (acc,count) = + let matching = Bit_utils.MatchType typ in + let offset', _ = Bit_utils.find_offset vi.vtype ~offset matching in + let node_kind = Scalar (vi, typ, offset') in + add (acc,count) node_kind in try - Ival.fold_int add_cells ival (acc,count) - with Abstract_interp.Error_Top -> raise NotACell + Ival.fold_int add_cell ival (acc,count) + with Abstract_interp.Error_Top | Bit_utils.NoMatchingOffset -> + (* fallback to composite node *) + add (acc,count) (Composite (vi)) end - | _ -> raise NotACell + | CLogic_Var _ -> add (acc,count) (Error "logic variables not supported") + | Null -> add (acc,count) AbsoluteMemory + | String (i,cs) -> add (acc,count) (String (i, cs)) in try fst (Location_Bits.fold_i add_base location.loc ([],0)) - with Abstract_interp.Error_Top | NoMatchingOffset -> raise NotACell + with Abstract_interp.Error_Top -> raise Unknown_location let build_node_kind ~is_folded_base lval kinstr = match enumerate_cells ~is_folded_base ~limit:1 lval kinstr with | [node_kind] -> node_kind - | _ | exception (NotACell | Too_many_deps _) -> Scattered (lval, kinstr) + | [] (* happens if kinstr is dead code *) -> Scattered (lval, kinstr) + | _ -> assert false + | exception (Too_many_deps _) -> Scattered (lval, kinstr) + | exception Unknown_location -> Unknown (lval, kinstr) let default_node_locality callstack = match callstack with @@ -310,23 +311,20 @@ let build_node context callstack lval kinstr = let build_all_scattered_node ~limit context callstack kinstr lval = let is_folded_base = is_folded context in - try - let cells, complete = - try - enumerate_cells ~is_folded_base ~limit lval kinstr, true - with Too_many_deps cells -> cells, false - in - let add node_kind = - let node = add_or_update_node context callstack node_kind in - let new_lval = Extlib.the (Node_kind.to_lval node_kind) in - update_node_values node kinstr new_lval; - node - in - List.map add cells, complete - with NotACell -> - Self.warning "Unable to enumerate cells for %a" - Cil_printer.pp_lval lval; - [], true + let cells, complete = + try + enumerate_cells ~is_folded_base ~limit lval kinstr, true + with Too_many_deps cells -> cells, false + in + let add 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; + node + in + List.map add cells, complete let build_var context callstack varinfo = let lval = Var varinfo, NoOffset in @@ -524,6 +522,8 @@ let build_node_deps context node = | Alarm (stmt,alarm) -> build_alarm_deps callstack stmt alarm; Done + | Unknown _ | AbsoluteMemory | String _ | Error _ -> + Done in node.node_writes_computation <- writes_computation; begin match Node_kind.get_base node.node_kind with @@ -587,8 +587,8 @@ let explore ~depth context root = let should_auto_explore node = let is_root = Graph.Node.equal node root (* the root is always explored *) and is_intersting_kind = match node.node_kind with - | Scalar _ | Composite _ | Alarm _ -> true | Scattered _ -> false + | _ -> true in is_root || (not node.node_hidden && is_intersting_kind) in @@ -597,7 +597,7 @@ let explore ~depth context root = Queue.add (root,0) queue; while not (Queue.is_empty queue) do let (n,d) = Queue.take queue in - if d < depth then begin + if d <= depth then begin if n.node_writes_computation <> Done && should_auto_explore n then build_node_deps context n; Graph.iter_pred (fun n' -> Queue.add (n',d+1) queue) context.graph n; diff --git a/src/plugins/dive/dive_graph.ml b/src/plugins/dive/dive_graph.ml index eede9ff4c8d188ff3fea0c505c1a1518a03e24a7..7b8b8162ad7c3e0a89531e9c977386021255d09d 100644 --- a/src/plugins/dive/dive_graph.ml +++ b/src/plugins/dive/dive_graph.ml @@ -252,9 +252,12 @@ let ouptput_to_dot out_channel g = | Scalar _ -> [`Shape `Box] | Composite _ -> [ `Shape `Box3d ] | Scattered _ -> [ `Shape `Parallelogram ] + | Unknown _ -> [`Shape `Diamond ; `Color 0xff0000] | Alarm _ -> [ `Shape `Doubleoctagon ; `Style `Bold ; `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xff0000 ] + | AbsoluteMemory | String _ -> [`Shape `Box3d] + | Error _ -> [`Color 0xff0000] and values = match grade with | None -> [] | Some Singleton -> @@ -310,7 +313,11 @@ struct | Scalar _ -> "scalar" | Composite _ -> "composite" | Scattered _ -> "scattered" + | Unknown _ -> "unknown" | Alarm _ -> "alarm" + | AbsoluteMemory -> "absolute" + | String _ -> "string" + | Error _ -> "error" in `String s diff --git a/src/plugins/dive/dive_types.mli b/src/plugins/dive/dive_types.mli index e8ca4d2e379f10113d8b7d5ef0f372fe94b7cadd..1acada506a32ca3852a7484a79fff2f5a5913aa7 100644 --- a/src/plugins/dive/dive_types.mli +++ b/src/plugins/dive/dive_types.mli @@ -24,7 +24,11 @@ type node_kind = | Scalar of Cil_types.varinfo * Cil_types.typ * Cil_types.offset | Composite of Cil_types.varinfo | Scattered of Cil_types.lval * Cil_types.kinstr + | Unknown of Cil_types.lval * Cil_types.kinstr | Alarm of Cil_types.stmt * Alarms.alarm + | AbsoluteMemory + | String of int * Base.cstring + | Error of string type node_locality = { loc_file : string; diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml index 30bfc795f823c6203fe8f01105f26400244c13eb..b52dd75817443a29118981186e3396a1b9db6304 100644 --- a/src/plugins/dive/node_kind.ml +++ b/src/plugins/dive/node_kind.ml @@ -55,8 +55,23 @@ struct LvalStructEq.compare lv1 lv2 <?> (Kinstr.compare, ki1, ki2) | Scattered _, _ -> 1 | _, Scattered _ -> -1 + | Unknown (lv1,ki1), Unknown (lv2,ki2) -> + LvalStructEq.compare lv1 lv2 <?> (Kinstr.compare, ki1, ki2) + | Unknown _, _ -> 1 + | _, Unknown _ -> -1 | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) -> Stmt.compare stmt1 stmt2 <?> (Alarms.compare, alarm1, alarm2) + | Alarm _, _ -> 1 + | _, Alarm _ -> -1 + | AbsoluteMemory, AbsoluteMemory -> 0 + | AbsoluteMemory, _ -> 1 + | _, AbsoluteMemory -> -1 + | String (i1,_), String (i2,_) -> + Datatype.Int.compare i1 i2 + | String _, _ -> 1 + | _, String _ -> -1 + | Error s1, Error s2 -> + Datatype.String.compare s1 s2 let equal k1 k2 = match k1, k2 with @@ -65,8 +80,13 @@ struct | Composite vi1, Composite vi2 -> Varinfo.equal vi1 vi2 | Scattered (lv1, ki1), Scattered (lv2, ki2) -> LvalStructEq.equal lv1 lv2 && Kinstr.equal ki1 ki2 + | Unknown (lv1, ki1), Unknown (lv2, ki2) -> + LvalStructEq.equal lv1 lv2 && Kinstr.equal ki1 ki2 | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) -> Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2 + | AbsoluteMemory, AbsoluteMemory -> true + | String (i,_), String (j,_) -> Datatype.Int.equal i j + | Error s1, Error s2 -> Datatype.String.equal s1 s2 | _ -> false let hash k = @@ -76,8 +96,13 @@ struct | Composite vi -> Hashtbl.hash (2, Varinfo.hash vi) | Scattered (lv, ki) -> Hashtbl.hash (3, LvalStructEq.hash lv, Kinstr.hash ki) + | Unknown (lv, ki) -> + Hashtbl.hash (4, LvalStructEq.hash lv, Kinstr.hash ki) | Alarm (stmt, alarm) -> - Hashtbl.hash (4, Stmt.hash stmt, Alarms.hash alarm) + Hashtbl.hash (5, Stmt.hash stmt, Alarms.hash alarm) + | AbsoluteMemory -> 6 + | String (i, _) -> Hashtbl.hash (7, i) + | Error s -> Hashtbl.hash (8, s) end include Datatype.Make (DatatypeInput) @@ -85,16 +110,26 @@ include Datatype.Make (DatatypeInput) let get_base = function | Scalar (vi,_,_) | Composite (vi) -> Some vi - | Scattered _ | Alarm _ -> None + | Scattered _ | Unknown _ | Alarm _ | AbsoluteMemory | String _ | 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 - | Alarm (_,_) -> None + | Unknown (lval,_) -> Some lval + | Alarm (_,_) | AbsoluteMemory | String _ | Error _ -> None let pretty fmt = function - | (Scalar _ | Composite _ | Scattered _) as kind -> + | (Scalar _ | Composite _ | Scattered _ | Unknown _) as kind -> Cil_printer.pp_lval fmt (Extlib.the (to_lval kind)) | Alarm (_stmt,alarm) -> Cil_printer.pp_predicate fmt (Alarms.create_predicate alarm) + | AbsoluteMemory -> + Format.fprintf fmt "%s" (Kernel.AbsoluteValidRange.get ()) + | String (_, CSString s) -> + Format.fprintf fmt "%S" s + | String (_, CSWstring s) -> + Format.fprintf fmt "L\"%s\"" (Escape.escape_wstring s) + | Error s -> + Format.fprintf fmt "%s" s diff --git a/src/plugins/dive/tests/dive/exceptional.i b/src/plugins/dive/tests/dive/exceptional.i new file mode 100644 index 0000000000000000000000000000000000000000..c65084f9539f908baf2ac70c605ddfe4efa437d1 --- /dev/null +++ b/src/plugins/dive/tests/dive/exceptional.i @@ -0,0 +1,24 @@ +/* run.config +STDOPT: +"-absolute-valid-range 0x10000000-0x1fffffff -dive-from-variables main::__retres -dive-depth-limit 5" +*/ + +int* gm(int *p) { return (int *) ((unsigned int) p * 2 / 2); } + + +int main(void) +{ + // String + char *s = "lorem ipsum"; + char c = s[4]; + + // Unknown + int i; + int *p = gm(&i); + int x = *p; + + // Absolute + int *r = 0x10000000; + int a = *r; + + return a + x + c; +} diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.dot b/src/plugins/dive/tests/dive/oracle/exceptional.dot new file mode 100644 index 0000000000000000000000000000000000000000..821e4f9d1ad1260921d9ac68892565b09d58db70 --- /dev/null +++ b/src/plugins/dive/tests/dive/oracle/exceptional.dot @@ -0,0 +1,26 @@ +digraph G { + cp1 [label=<__retres>, shape=box, ]; + cp2 [label=<a>, shape=box, fillcolor="#FFBBBB", color="#FF0000", + style="filled", ]; + cp4 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000", + style="filled", ]; + cp6 [label=<c>, shape=box, fillcolor="#AACCFF", color="#88AAFF", + style="filled", ]; + cp8 [label=<0x10000000-0x1fffffff>, shape=box3d, fillcolor="#FFBBBB", + color="#FF0000", style="filled", ]; + cp10 [label=<*p>, shape=parallelogram, fillcolor="#FFBBBB", + color="#FF0000", style="filled,dotted", ]; + cp12 [label=<"lorem ipsum">, shape=box3d, fillcolor="#AACCFF", + color="#88AAFF", style="filled", ]; + + subgraph cluster_cs_1 { label=<main>; cp12;cp10;cp8;cp6;cp4;cp2;cp1; + }; + + cp2 -> cp1; + cp4 -> cp1; + cp6 -> cp1; + cp8 -> cp2; + cp10 -> cp4; + cp12 -> cp6; + + } \ No newline at end of file diff --git a/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..36f7c9648b859d37d957e47a97582ffb50813080 --- /dev/null +++ b/src/plugins/dive/tests/dive/oracle/exceptional.res.oracle @@ -0,0 +1,39 @@ +[kernel] Parsing tests/dive/exceptional.i (no preprocessing) +[eva] Analyzing a complete application starting at main +[eva] Computing initial state +[eva] Initial state computed +[eva] tests/dive/exceptional.i:5: + Assigning imprecise value to __retres. + The imprecision originates from Arithmetic {tests/dive/exceptional.i:5} +[eva] tests/dive/exceptional.i:5: + Assigning imprecise value to \result<gm>. + The imprecision originates from Arithmetic {tests/dive/exceptional.i:5} +[eva] tests/dive/exceptional.i:16: + Assigning imprecise value to p. + The imprecision originates from Arithmetic {tests/dive/exceptional.i:5} +[eva:alarm] tests/dive/exceptional.i:17: Warning: + accessing uninitialized left-value. assert \initialized(p); +[eva:alarm] tests/dive/exceptional.i:17: Warning: + out of bounds read. assert \valid_read(p); +[eva:alarm] tests/dive/exceptional.i:23: Warning: + signed overflow. assert -2147483648 ≤ a + x; +[eva:alarm] tests/dive/exceptional.i:23: Warning: + signed overflow. assert a + x ≤ 2147483647; +[eva:alarm] tests/dive/exceptional.i:23: Warning: + signed overflow. assert (int)(a + x) + (int)c ≤ 2147483647; +[eva] done for function main +[eva:summary] ====== ANALYSIS SUMMARY ====== + ---------------------------------------------------------------------------- + 2 functions analyzed (out of 2): 100% coverage. + In these functions, 10 statements reached (out of 10): 100% coverage. + ---------------------------------------------------------------------------- + No errors or warnings raised during the analysis. + ---------------------------------------------------------------------------- + 5 alarms generated by the analysis: + 1 invalid memory access + 3 integer overflows + 1 access to uninitialized left-values + ---------------------------------------------------------------------------- + No logical properties have been reached by the analysis. + ---------------------------------------------------------------------------- +[dive] output to tests/dive/result/exceptional.dot