Replace some folds with exists or for_all

.semgrep/fold.yml

@@ -0,0 +1,26 @@
+rules:
+  - id: fold-exists
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... false
+        - pattern: $D.fold_left ... false
+        - pattern: $D.fold_right ... false
+        - pattern: fold ... false
+        - pattern: fold_left ... false
+        - pattern: fold_right ... false
+    message: consider replacing fold with exists
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: fold-for_all
+    patterns:
+      - pattern-either:
+        - pattern: $D.fold ... true
+        - pattern: $D.fold_left ... true
+        - pattern: $D.fold_right ... true
+        - pattern: fold ... true
+        - pattern: fold_left ... true
+        - pattern: fold_right ... true
+    message: consider replacing fold with for_all
+    languages: [ocaml]
+    severity: WARNING

src/analyses/basePriv.ml

@@ -1040,11 +1040,11 @@ struct
     let s = MustLockset.remove m (current_lockset ask) in
     let t = current_thread ask in
     let side_cpa = CPA.filter (fun x _ ->
-        GWeak.fold (fun s' tm acc ->
+        GWeak.exists (fun s' tm ->
             (* TODO: swap 2^M and T partitioning for lookup by t here first? *)
             let v = ThreadMap.find t tm in
-            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
-          ) (G.weak (getg (V.global x))) false
+            (MustLockset.mem m s' && not (VD.is_bot v))
+          ) (G.weak (getg (V.global x)))
       ) st.cpa
     in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
@@ -1098,9 +1098,9 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let s = MustLockset.remove m (current_lockset ask) in
     let side_cpa = CPA.filter (fun x _ ->
-        GWeak.fold (fun s' v acc ->
-            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
-          ) (G.weak (getg (V.global x))) false
+        GWeak.exists (fun s' v ->
+            (MustLockset.mem m s' && not (VD.is_bot v))
+          ) (G.weak (getg (V.global x)))
       ) st.cpa
     in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));

src/domain/partitionDomain.ml

@@ -31,10 +31,10 @@ struct
   let meet _ _ = failwith "PartitonDomain.Set.meet: unsound"
 
   let collapse (s1:t) (s2:t): bool =
-    let f vf2 res =
-      res || exists (fun vf1 -> S.collapse vf1 vf2) s1
+    let f vf2 =
+      exists (fun vf1 -> S.collapse vf1 vf2) s1
     in
-    fold f s2 false
+    exists f s2
 
   let add e s = join s (singleton e)
 

src/incremental/compareCFG.ml

@@ -131,7 +131,7 @@
           false
         end in
     let cond n2 = Node.equal n2 (FunctionEntry f2) || check_all_nodes_in_same (List.map snd (CfgNew.prev n2)) n2 in
-    let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in
+    let forall = NH.fold (fun n2 n1 acc -> acc && cond n2) same.node2to1 true in (* nosemgrep: fold-for_all *) (* cond does side effects *)
     if not forall then repeat () in
   repeat ();
   NH.to_seq same.node1to2, NH.to_seq_keys diffNodes1

src/solver/td3.ml

@@ -289,7 +289,7 @@ module Base =
               destabilize_vs y || b || was_stable && List.mem_cmp S.Var.compare y vs
             else
               true
-          ) w false
+          ) w false (* nosemgrep: fold-exists *) (* does side effects *)
       and solve ?reuse_eq x phase =
         if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x);
         init x;

src/witness/witness.ml

@@ -342,14 +342,14 @@ struct
     | UnreachCall _ ->
       (* error function name is globally known through Svcomp.task *)
       let is_unreach_call =
-        LHT.fold (fun (n, c) v acc ->
+        LHT.for_all (fun (n, c) v ->
             match n with
             (* FunctionEntry isn't used for extern __VERIFIER_error... *)
             | FunctionEntry f when Svcomp.is_error_function f.svar ->
               let is_dead = Spec.D.is_bot v in
-              acc && is_dead
-            | _ -> acc
-          ) lh true
+              is_dead
+            | _ -> true
+          ) lh
       in
 
       if is_unreach_call then (