[dive] handle (hopefully) all exceptional cases

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;

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
 

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;

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

src/plugins/dive/tests/dive/exceptional.i

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

src/plugins/dive/tests/dive/oracle/exceptional.dot

+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

src/plugins/dive/tests/dive/oracle/exceptional.res.oracle

+[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