Merge pull request #783 from goblint/issue_55

Categorize Remaining Warnings

src/analyses/arinc.ml

@@ -5,8 +5,6 @@ open Analyses
 
 module BI = IntOps.BigIntOps
 
-let debug_doc doc = M.debug "%a" Pretty.insert doc
-
 module Functions = struct
   let prefix = "LAP_Se_"
   (* ARINC functions copied from stdapi.c *)
@@ -37,7 +35,7 @@ module Functions = struct
         Some (
             let ret = if GobConfig.get_bool "ana.arinc.assume_success" then ret_success else if List.mem fname with_timeout then ret_any else ret_no_timeout in
             let v = vd ret in
-            debug_doc @@ Pretty.dprintf "effect of %s: set %a to %a" fname d_lval lv ValueDomain.Compound.pretty v;
+            M.debug ~category:Analyzer "effect of %s: set %a to %a" fname d_lval lv ValueDomain.Compound.pretty v;
             [(lv, v)]
           )
       | _ -> None
@@ -144,25 +142,24 @@ struct
   let dummy_global_dlval = { dummyFunDec.svar with vname = "Gret" }, `NoOffset
   let global_dlval dlval fname =
     if Lval.CilLval.class_tag dlval = `Global then (
-      M.debug "WARN: %s: use of global lval: %s" fname (str_return_dlval dlval);
+      M.debug ~category:Analyzer "WARN: %s: use of global lval: %s" fname (str_return_dlval dlval);
       if GobConfig.get_bool "ana.arinc.merge_globals" then dummy_global_dlval else dlval
     ) else dlval
   let mayPointTo ctx exp =
     match ctx.ask (Queries.MayPointTo exp) with
     | a when not (Queries.LS.is_top a) && Queries.LS.cardinal a > 0 ->
       let top_elt = (dummyFunDec.svar, `NoOffset) in
       let a' = if Queries.LS.mem top_elt a then (
-          M.debug "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
+          M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
           Queries.LS.remove top_elt a
         ) else a
       in
       Queries.LS.elements a'
     | v ->
-      M.debug "mayPointTo: query result for %a is %a" d_exp exp Queries.LS.pretty v;
+      M.info ~category:Unsound "mayPointTo: query result for %a is %a, ignoring it" d_exp exp Queries.LS.pretty v;
       (*failwith "mayPointTo"*)
       []
   let iterMayPointTo ctx exp f = mayPointTo ctx exp |> List.iter f
-  let debugMayPointTo ctx exp = M.debug "%a mayPointTo %a" d_exp exp (Pretty.d_list ", " Lval.CilLval.pretty) (mayPointTo ctx exp)
 
 
   (* transfer functions *)
@@ -178,13 +175,13 @@ struct
       (* OPT: this matching is just for speed up to avoid querying on every assign *)
       match lval with Var _, _ when not @@ is_return_code_type (Lval lval) -> ctx.local | _ ->
         (* TODO why is it that current_node can be None here, but not in other transfer functions? *)
-        if not @@ Option.is_some !MyCFG.current_node then (M.debug "assign: MyCFG.current_node not set :("; ctx.local) else
+        if not @@ Option.is_some !MyCFG.current_node then (M.info ~category:Unsound ~tags:[Category Analyzer] "assign: MyCFG.current_node not set :("; ctx.local) else
         if D.is_bot1 ctx.local then ctx.local else
           let env = get_env ctx in
           let edges_added = ref false in
           let f dlval =
             (* M.debug @@ "assign: MayPointTo " ^ sprint d_plainlval lval ^ ": " ^ sprint d_plainexp (Lval.CilLval.to_exp dlval); *)
-            let is_ret_type = try is_return_code_type @@ Lval.CilLval.to_exp dlval with Cilfacade.TypeOfError Index_NonArray -> M.debug "assign: Cilfacade.typeOf %a threw exception Errormsg.Error \"Bug: typeOffset: Index on a non-array\". Will assume this is a return type to remain sound." d_exp (Lval.CilLval.to_exp dlval); true in
+            let is_ret_type = try is_return_code_type @@ Lval.CilLval.to_exp dlval with Cilfacade.TypeOfError Index_NonArray -> M.debug ~category:Imprecise "assign: Cilfacade.typeOf %a threw exception Errormsg.Error \"Bug: typeOffset: Index on a non-array\". Will assume this is a return type to remain sound." d_exp (Lval.CilLval.to_exp dlval); true in
             if (not is_ret_type) || Lval.CilLval.has_index dlval then () else
               let dlval = global_dlval dlval "assign" in
               edges_added := true;
@@ -222,7 +219,7 @@ struct
                let else_node = NodeTbl.get @@ Branch (List.hd else_stmts) in
                let dst_node = if tv then then_node else else_node in
                let d_if = if List.compare_length_with stmt.preds 1 > 0 then ( (* seems like this never happens *)
-                   M.debug "WARN: branch: If has more than 1 predecessor, will insert Nop edges!";
+                   M.debug ~category:Analyzer "WARN: branch: If has more than 1 predecessor, will insert Nop edges!";
                    add_edges env ArincUtil.Nop;
                    { ctx.local with pred = Pred.of_node env.node }
                  ) else ctx.local
@@ -249,14 +246,9 @@ struct
         | BinOp(Ne, a, b, _) -> check (stripCasts a) (stripCasts b) (not tv)
         | _ -> ctx.local
 
-  let checkPredBot d tf f xs =
-    if d.pred = Pred.bot () then M.debug "%s: mapping is BOT!!! function: %s. %a" tf f.vname (Pretty.d_list "\n" (fun () (n, d) -> Pretty.dprintf "%s = %a" n Pred.pretty d.pred)) xs;
-    d
-
   let body ctx (f:fundec) : D.t = (* enter is not called for spawned processes -> initialize them here *)
-    (* M.debug @@ "BODY " ^ f.svar.vname ^" @ "^ string_of_int (!Tracing.current_loc).line; *)
+    (* M.debug ~category:Analyzer @@ "BODY " ^ f.svar.vname ^" @ "^ string_of_int (!Tracing.current_loc).line; *)
     (* if not (is_single ctx || !Goblintutil.global_initialization || fst (ctx.global part_mode_var)) then raise Analyses.Deadcode; *)
-    (* checkPredBot ctx.local "body" f.svar [] *)
     let module BaseMain = (val Base.get_main ()) in
     let base_context = BaseMain.context_cpa f @@ Obj.obj @@ ctx.presub "base" in
     let context_hash = Hashtbl.hash (base_context, ctx.local.pid) in
@@ -266,7 +258,6 @@ struct
     ctx.local
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = (* on function calls (also for main); not called for spawned processes *)
-    (* print_endline @@ "ENTER " ^ f.vname ^" @ "^ string_of_int (!Tracing.current_loc).line; (* somehow M.debug doesn't print anything here *) *)
     let d_caller = ctx.local in
     let d_callee = if D.is_bot ctx.local then ctx.local else { ctx.local with pred = Pred.of_node (MyCFG.Function f); ctx = Ctx.top () } in (* set predecessor set to start node of function *)
     [d_caller, d_callee]
@@ -319,8 +310,7 @@ struct
       let is_arinc_fun = startsWith Functions.prefix f.vname in
       let is_creating_fun = startsWith (Functions.prefix^"Create") f.vname in
       if M.tracing && is_arinc_fun then (
-        (* M.tracel "arinc" "found %s(%s)\n" f.vname args_str *)
-        M.debug "found %s(%a) in %s" f.vname (Pretty.d_list ", " d_exp) arglist env.fundec.svar.vname
+        M.tracel "arinc" "found %s(%a) in %s" f.vname (Pretty.d_list ", " d_exp) arglist env.fundec.svar.vname
       );
       let is_error_handler = env.pname = pname_ErrorHandler in
       let eval_int exp =
@@ -358,7 +348,7 @@ struct
             let f dlval =
               let dlval = global_dlval dlval "special" in
               if not @@ is_return_code_type @@ Lval.CilLval.to_exp dlval
-              then (M.debug "WARN: last argument in arinc function may point to something other than a return code: %s" (str_return_dlval dlval); None)
+              then (M.debug ~category:Analyzer "WARN: last argument in arinc function may point to something other than a return code: %s" (str_return_dlval dlval); None)
               else (add_return_dlval env `Write dlval; Some (str_return_dlval dlval))
             in
             (* add actions for all lvals r may point to *)
@@ -412,7 +402,7 @@ struct
         (* | "F62", [dst; src; len] (* strncmp *) *)
         (* | "F63", [dst; src; len] (* memcpy *) *)
         ->
-        M.debug @@ "strcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^")";
+        M.debug ~category:Analyzer @@ "strcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^")";
         (*debugMayPointTo ctx dst;*)
         assert_ptr dst; assert_ptr src;
         (* let dst_lval = mkMem ~addr:dst ~off:NoOffset in *)
@@ -421,12 +411,12 @@ struct
         | ls ->
             ignore @@ Pretty.printf "strcpy %a points to %a\n" d_exp dst Queries.LS.pretty ls;
             Queries.LS.iter (fun (v,o) -> ctx.assign ~name:"base" (Var v, Lval.CilLval.to_ciloffs o) src) ls
-        | _ -> M.debug @@ "strcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^"): dst may point to anything!";
+        | _ -> M.debug ~category:Analyzer @@ "strcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^"): dst may point to anything!";
         end;
         d
       | "F63" , [dst; src; len] (* memcpy *)
         ->
-        M.debug @@ "memcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^")";
+        M.debug ~category:Analyzer @@ "memcpy/"^f.vname^"("^sprint d_plainexp dst^", "^sprint d_plainexp src^")";
         (match ctx.ask (Queries.EvalInt len) with
          | `Int i ->
            (*
@@ -441,7 +431,7 @@ struct
            let dst_lval = mkMem ~addr:dst ~off:NoOffset in
            let src_lval = mkMem ~addr:src ~off:NoOffset in
            ctx.assign ~name:"base" dst_lval (Lval src_lval); (* this is only ok because we use ArrayDomain.Trivial per default, i.e., there's no difference between the first element or the whole array *)
-         | v -> M.debug @@ "F63/memcpy: don't know length: " ^ sprint Queries.Result.pretty v;
+         | v -> M.debug ~category:Analyzer @@ "F63/memcpy: don't know length: " ^ sprint Queries.Result.pretty v;
            let lval = mkMem ~addr:dst ~off:NoOffset in
            ctx.assign ~name:"base" lval MyCFG.unknown_exp
         );
@@ -460,7 +450,7 @@ struct
            *)
            let dst_lval = mkMem ~addr:dst ~off:NoOffset in
            ctx.assign ~name:"base" dst_lval data; (* this is only ok because we use ArrayDomain.Trivial per default, i.e., there's no difference between the first element or the whole array *)
-         | v -> M.debug @@ "F1/memset: don't know length: " ^ sprint Queries.Result.pretty v;
+         | v -> M.debug ~category:Analyzer @@ "F1/memset: don't know length: " ^ sprint Queries.Result.pretty v;
            let lval = mkMem ~addr:dst ~off:NoOffset in
            ctx.assign ~name:"base" lval MyCFG.unknown_exp
         );
@@ -504,7 +494,7 @@ struct
             let pid' = Process, name in
             assign_id pid (get_id pid');
             add_actions (List.map (fun f -> CreateProcess Action.({ pid = pid'; f; pri; per; cap })) funs)
-          | _ -> let f (type a) (x: a Queries.result) = "TODO" in struct_fail (M.debug "%s") (`Result (f name, f entry_point, f pri, f per, f cap)); d (* TODO: f*)
+          | _ -> let f (type a) (x: a Queries.result) = "TODO" in struct_fail (M.debug ~category:Analyzer "%s") (`Result (f name, f entry_point, f pri, f per, f cap)); d (* TODO: f*)
         end
       | "LAP_Se_GetProcessId", [name; pid; r] ->
         assign_id_by_name Process name pid; d

src/analyses/base.ml

@@ -415,7 +415,7 @@ struct
     match value with
     | `Top ->
       if VD.is_immediate_type t then () else M.info ~category:Unsound "Unknown value in %s could be an escaped pointer address!" description; empty
-    | `Bot -> (*M.debug "A bottom value when computing reachable addresses!";*) empty
+    | `Bot -> (*M.debug ~category:Analyzer "A bottom value when computing reachable addresses!";*) empty
     | `Address adrs when AD.is_top adrs ->
       M.info ~category:Unsound "Unknown address in %s has escaped." description; AD.remove Addr.NullPtr adrs (* return known addresses still to be a bit more sane (but still unsound) *)
     (* The main thing is to track where pointers go: *)
@@ -766,7 +766,7 @@ struct
                     if contains_vla t || contains_vla (get_type_addr (x, o)) then
                       begin
                         (* TODO: Is this ok? *)
-                        M.warn "Casting involving a VLA is assumed to work";
+                        M.info ~category:Unsound "Casting involving a VLA is assumed to work";
                         true
                       end
                     else
@@ -994,7 +994,6 @@ struct
     let r = match eval_rv_no_ask_evalint ask gs st e with
       | `Int i -> `Lifted i (* cast should be unnecessary, eval_rv should guarantee right ikind already *)
       | `Bot   -> Queries.ID.top () (* out-of-scope variables cause bot, but query result should then be unknown *)
-      (* | v      -> M.warn ("Query function answered " ^ (VD.show v)); Queries.Result.top q *)
       | v      -> M.debug ~category:Analyzer "Base EvalInt %a query answering bot instead of %a" d_exp e VD.pretty v; Queries.ID.bot ()
     in
     if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a\n" d_exp e Queries.ID.pretty r;
@@ -1022,15 +1021,18 @@ struct
     | _ -> None
 
   let eval_funvar ctx fval: varinfo list =
+    let exception OnlyUnknown in
     try
       let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
       if AD.mem Addr.UnknownPtr fp then begin
-        M.warn "Function pointer %a may contain unknown functions." d_exp fval;
-        dummyFunDec.svar :: AD.to_var_may fp
+        let others = AD.to_var_may fp in
+        if others = [] then raise OnlyUnknown;
+        M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval;
+        dummyFunDec.svar :: others
       end else
         AD.to_var_may fp
-    with SetDomain.Unsupported _ ->
-      M.warn "Unknown call to function %a." d_exp fval;
+    with SetDomain.Unsupported _ | OnlyUnknown ->
+      M.warn ~category:Unsound "Unknown call to function %a." d_exp fval;
       [dummyFunDec.svar]
 
   (** Evaluate expression as address.
@@ -1161,7 +1163,6 @@ struct
     | Q.EvalFunvar e ->
       begin
         let fs = eval_funvar ctx e in
-        (*          Messages.warn ~msg:("Base: I should know it! "^string_of_int (List.length fs)) ();*)
         List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
       end
     | Q.EvalInt e ->
@@ -1322,7 +1323,7 @@ struct
             with Cilfacade.TypeOfError _ ->
               (* If we cannot determine the correct type here, we go with the one of the LVal *)
               (* This will usually lead to a type mismatch in the ValueDomain (and hence supertop) *)
-              M.warn "Cilfacade.typeOfLval failed Could not obtain the type of %a" d_lval (Var x, cil_offset);
+              M.debug ~category:Analyzer "Cilfacade.typeOfLval failed Could not obtain the type of %a" d_lval (Var x, cil_offset);
               lval_type
       in
       let update_offset old_value =
@@ -1455,7 +1456,7 @@ struct
     (* If any of the addresses are unknown, we ignore it!?! *)
     | SetDomain.Unsupported x ->
       (* if M.tracing then M.tracel "set" ~var:firstvar "set got an exception '%s'\n" x; *)
-      M.warn "Assignment to unknown address"; st
+      M.info ~category:Unsound "Assignment to unknown address, assuming no write happened."; st
 
   let set_many ~ctx a (gs:glob_fun) (st: store) lval_value_list: store =
     (* Maybe this can be done with a simple fold *)
@@ -1659,7 +1660,7 @@ struct
     let inv_bin_int (a, b) ikind c op =
       let warn_and_top_on_zero x =
         if GobOption.exists (BI.equal BI.zero) (ID.to_int x) then
-          (M.warn "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
+          (M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Must Undefined Behavior: Second argument of div or mod is 0, continuing with top";
           ID.top_of ikind)
         else
           x
@@ -1922,7 +1923,7 @@ struct
     let rval_val = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local rval in
     let lval_val = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
     (* let sofa = AD.short 80 lval_val^" = "^VD.short 80 rval_val in *)
-    (* M.debug @@ sprint ~width:80 @@ dprintf "%a = %a\n%s" d_plainlval lval d_plainexp rval sofa; *)
+    (* M.debug ~category:Analyzer @@ sprint ~width:80 @@ dprintf "%a = %a\n%s" d_plainlval lval d_plainexp rval sofa; *)
     let not_local xs =
       let not_local x =
         match Addr.to_var_may x with
@@ -1983,7 +1984,6 @@ struct
       match ctx.ask (Queries.CondVars exp) with
       | s when Queries.ES.cardinal s = 1 ->
         let e = Queries.ES.choose s in
-        M.debug "CondVars result for expression %a is %a" d_exp exp d_exp e;
         invariant ctx (Analyses.ask_of_ctx ctx) ctx.global res e tv
       | _ -> res
     in
@@ -2039,7 +2039,7 @@ struct
       | None -> nst
       | Some exp ->
         let t_override = match Cilfacade.fundec_return_type fundec with
-          | TVoid _ -> M.warn "Returning a value from a void function"; assert false
+          | TVoid _ -> M.warn ~category:M.Category.Program "Returning a value from a void function"; assert false
           | ret -> ret
         in
         let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local exp in
@@ -2261,12 +2261,12 @@ struct
       if not change then ctx.local else begin
         let newst = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local e true in
         (* if check_assert e newst <> `Lifted true then
-            M.warn ~msg:("Invariant \"" ^ expr ^ "\" does not stick.") (); *)
+            M.warn ~category:Assert ~msg:("Invariant \"" ^ expr ^ "\" does not stick.") (); *)
         newst
       end
 
   let special_unknown_invalidate ctx ask gs st f args =
-    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn "Unknown function ptr called");
+    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise "Unknown function ptr called");
     let desc = LF.find f in
     let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
     let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in

src/analyses/condVars.ml

@@ -64,7 +64,7 @@ struct
     | a when not (Queries.LS.is_top a) && Queries.LS.cardinal a > 0 ->
       let top_elt = (dummyFunDec.svar, `NoOffset) in
       let a' = if Queries.LS.mem top_elt a then (
-          M.debug "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
+          M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
           Queries.LS.remove top_elt a
         ) else a
       in
@@ -104,7 +104,7 @@ struct
     let save_expr lval expr =
       match mustPointTo ctx (AddrOf lval) with
       | Some clval ->
-        M.debug "CondVars: saving %a = %a" Lval.CilLval.pretty clval d_exp expr;
+        if M.tracing then M.tracel "condvars" "CondVars: saving %a = %a" Lval.CilLval.pretty clval d_exp expr;
         D.add clval (D.V.singleton expr) d (* if lval must point to clval, add expr *)
       | None -> d
     in