Merge branch 'master' into multishot-svcomp25

Author: DrMichaelPetter

.semgrep/let.yml

@@ -0,0 +1,6 @@
+rules:
+  - id: let-unit-in
+    pattern: let () = $E in ...
+    message: use ; instead (and, if needed, add surrounding parentheses to preserve precedence)
+    languages: [ocaml]
+    severity: WARNING

src/analyses/apron/apronAnalysis.apron.ml

@@ -36,7 +36,7 @@ let () =
   Printexc.register_printer
     (function
       | Apron.Manager.Error e ->
-        let () = Apron.Manager.print_exclog Format.str_formatter e in
-        Some(Printf.sprintf "Apron.Manager.Error\n %s" (Format.flush_str_formatter ()))
+        Apron.Manager.print_exclog Format.str_formatter e;
+        Some (Printf.sprintf "Apron.Manager.Error\n %s" (Format.flush_str_formatter ()))
       | _ -> None (* for other exceptions *)
     )

src/analyses/memOutOfBounds.ml

@@ -269,7 +269,7 @@ struct
           | None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
         end in
         let e_size = get_size_of_ptr_target man e in
-        let () = begin match e_size with
+        begin match e_size with
           | `Top ->
             (set_mem_safety_flag InvalidDeref;
              M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e)
@@ -297,7 +297,7 @@ struct
                 (set_mem_safety_flag InvalidDeref;
                  M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs)
             end
-        end in
+        end;
         begin match e with
           | Lval (Var v, _) as lval_exp -> check_no_binop_deref man lval_exp
           | BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI ->

src/analyses/varEq.ml

@@ -17,12 +17,16 @@ struct
   struct
     include PartitionDomain.ExpPartitions
 
+    let is_str_constant = function
+      | Const (CStr _ | CWStr _) -> true
+      | _ -> false
+
     let invariant ~scope ss =
       fold (fun s a ->
           if B.mem MyCFG.unknown_exp s then
             a
           else (
-            let s' = B.filter (fun x -> not (InvariantCil.exp_contains_tmp x) && InvariantCil.exp_is_in_scope scope x) s in
+            let s' = B.filter (fun x -> not (InvariantCil.exp_contains_tmp x) && InvariantCil.exp_is_in_scope scope x && not (is_str_constant x)) s in
             if B.cardinal s' >= 2 then (
               (* instead of returning quadratically many pairwise equalities from a cluster,
                  output linear number of equalities with just one expression *)

src/arg/myARG.ml

@@ -156,7 +156,7 @@ struct
     | n :: stack ->
       let cfgnode = Arg.Node.cfgnode n in
       match cfgnode with
-      | Function _ -> (* TODO: can this be done without cfgnode? *)
+      | Function cfgnode_fd -> (* TODO: can this be done without cfgnode? *)
         begin match stack with
           (* | [] -> failwith "StackArg.next: return stack empty" *)
           | [] -> [] (* main return *)
@@ -171,14 +171,33 @@ struct
                   | _ -> None
                 )
             in
+            let (entry_lval, entry_args) =
+              Arg.next call_n
+              (* filter because infinite loops starting with function call
+                 will have another Neg(1) edge from the head *)
+              |> List.filter_map (fun (edge, to_n) ->
+                  match edge with
+                  | InlineEntry (lval, _, args) -> Some (lval, args)
+                  | _ -> None
+                )
+              |> List.sort_uniq [%ord: CilType.Lval.t option * CilType.Exp.t list] (* TODO: deduplicate unique element in O(n) *)
+              |> (function
+                  | [lval_args] -> lval_args
+                  | _ -> assert false (* all calls from a node must have same args and lval, even if called function might be different via function pointer *)
+                )
+            in
             Arg.next n
             |> List.filter_map (fun (edge, to_n) ->
-                if BatList.mem_cmp Arg.Node.compare to_n call_next then (
-                  let to_n' = to_n :: call_stack in
-                  Some (edge, to_n')
-                )
-                else
-                  None
+                match edge with
+                | InlineReturn (lval, fd, args) ->
+                  assert (CilType.Fundec.equal fd cfgnode_fd); (* fd in return node should be the same as in InlineReturn edge *)
+                  if BatList.mem_cmp Arg.Node.compare to_n call_next && [%eq: CilType.Lval.t option] lval entry_lval && [%eq: CilType.Exp.t list] args entry_args then (
+                    let to_n' = to_n :: call_stack in
+                    Some (edge, to_n')
+                  )
+                  else
+                    None
+                | _ -> assert false
               )
         end
       | _ ->

src/cdomain/value/domains/invariantCil.ml

@@ -26,15 +26,23 @@ let exp_deep_unroll_types =
   let visitor = new exp_deep_unroll_types_visitor in
   visitCilExpr visitor
 
+let var_may_be_shadowed scope vi =
+  let vi_original_name = Cilfacade.find_original_name vi in
+  let local_may_shadow local =
+    not (CilType.Varinfo.equal vi local) && (* exclude self-equality by vid because the original names would always equal *)
+    vi_original_name = Cilfacade.find_original_name local
+  in
+  List.exists local_may_shadow scope.sformals || List.exists local_may_shadow scope.slocals
 
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
-  | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
+  | None ->
+    vi.vstorage <> Static && (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
+    not (var_may_be_shadowed scope vi)
   | Some fd ->
-    if CilType.Fundec.equal fd scope then
-      GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
-    else
-      false
+    CilType.Fundec.equal fd scope &&
+    (GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)) &&
+    not (var_may_be_shadowed scope vi) (* TODO: could distinguish non-nested and nested? *)
 
 class exp_is_in_scope_visitor (scope: fundec) (acc: bool ref) = object
   inherit nopCilVisitor

src/solver/sLRterm.ml

@@ -49,13 +49,13 @@ module SLR3term =
       let count  = ref 0 in
       let count_side  = ref (max_int - 1) in
 
-      let () = print_solver_stats := fun () ->
+      print_solver_stats := (fun () ->
           Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side);
           let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *)
           HM.iter (fun k _ -> Hashtbl.modify_def 1 (S.Var.var_id k) ((+)1) histo) rho;
           let vid,n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in
           Logs.info "max #contexts: %d for var_id %s" n vid
-      in
+        );
 
       let init ?(side=false) x =
         if not (HM.mem rho x) then begin

src/solver/td3.ml

@@ -287,11 +287,11 @@ module Base =
         include WPS (EqS) (HM) (VS)
       end in
 
-      let () = print_solver_stats := fun () ->
+      print_solver_stats := (fun () ->
           print_data data;
           Logs.info "|called|=%d" (HM.length called);
           print_context_stats rho
-      in
+        );
 
       if GobConfig.get_bool "incremental.load" then (
         print_data_verbose data "Loaded data for incremental analysis";

src/solver/td_simplified.ml

@@ -24,14 +24,14 @@ module Base : GenericEqSolver =
       let wpoint = HM.create 10 in
       let stable = HM.create 10 in
 
-      let () = print_solver_stats := fun () ->
+      print_solver_stats := (fun () ->
           Logs.debug "|rho|=%d" (HM.length rho);
           Logs.debug "|stable|=%d" (HM.length stable);
           Logs.debug "|infl|=%d" (HM.length infl);
           Logs.debug "|wpoint|=%d" (HM.length wpoint);
           Logs.info "|called|=%d" (HM.length called);
           print_context_stats rho
-      in
+        );
 
       let add_infl y x =
         if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
@@ -122,7 +122,7 @@ module Base : GenericEqSolver =
               if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
               box old eqd)
           in
-          if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( 
+          if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
             (* old != wpd *)
             if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old);
             update_var_event x old wpd;
@@ -132,7 +132,7 @@ module Base : GenericEqSolver =
             (iterate[@tailcall]) x
           ) else (
             (* old == wpd *)
-            if not (HM.mem stable x) then ( 
+            if not (HM.mem stable x) then (
               (* value unchanged, but not stable, i.e. destabilized itself during rhs *)
               if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
               (iterate[@tailcall]) x
@@ -172,7 +172,7 @@ module Base : GenericEqSolver =
           );
           List.iter (fun x -> HM.replace called x ();
                       if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
-                      iterate x; 
+                      iterate x;
                       HM.remove called x
                     ) unstable_vs;
           solver ();

src/solver/td_simplified_ref.ml

@@ -28,9 +28,9 @@ module Base : GenericEqSolver =
     let solve st vs =
       let (data : var_data ref HM.t) = HM.create 10 in
 
-      let () = print_solver_stats := fun () ->
+      print_solver_stats := (fun () ->
           Logs.debug "|data|=%d" (HM.length data);
-      in
+        );
 
       let add_infl y x =
         if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
@@ -46,12 +46,12 @@ module Base : GenericEqSolver =
           begin
             new_var_event x;
             if tracing then trace "init" "init %a" S.Var.pretty_trace x;
-            let data_x = ref { 
+            let data_x = ref {
                 infl = VS.empty;
                 value = S.Dom.bot ();
                 wpoint = false;
                 stable = false;
-                called = false 
+                called = false
               } in
             HM.replace data x data_x;
             data_x
@@ -138,7 +138,7 @@ module Base : GenericEqSolver =
               if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
               box old eqd)
           in
-          if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( 
+          if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
             (* old != wpd *)
             if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old);
             update_var_event x old wpd;
@@ -148,7 +148,7 @@ module Base : GenericEqSolver =
             (iterate[@tailcall]) x
           ) else (
             (* old == wpd *)
-            if not (!x_ref.stable) then ( 
+            if not (!x_ref.stable) then (
               (* value unchanged, but not stable, i.e. destabilized itself during rhs *)
               if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
               (iterate[@tailcall]) x
@@ -185,12 +185,12 @@ module Base : GenericEqSolver =
             Logs.newline ();
             flush_all ();
           );
-          List.iter (fun x -> 
+          List.iter (fun x ->
               let x_ref = HM.find data x in
               x_ref := { !x_ref with called = true };
               if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
-              iterate x; 
-              x_ref := { !x_ref with called = false } 
+              iterate x;
+              x_ref := { !x_ref with called = false }
             ) unstable_vs;
           solver ();
         )