Add semgrep rules for List.length and List.combine

.semgrep/list.yml

@@ -0,0 +1,61 @@
+rules:
+  - id: list-length-compare-0
+    pattern-either:
+      - pattern: List.length $L = 0
+      - pattern: List.length $L <> 0
+      - pattern: List.length $L > 0
+      - pattern: List.length $L >= 1
+      # doesn't find in ValueDomain: List.length ci.cfields > 0
+      # doesn't find in MyLiveness: List.length s.labels = 0
+    message: computing list length is inefficient for emptiness checking, compare with [] instead
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: list-length-compare-n
+    patterns:
+      - pattern-either:
+        - pattern: List.length $L = $N
+        - pattern: List.length $L <> $N
+        - pattern: List.length $L > $N
+        - pattern: List.length $L >= $N
+        - pattern: List.length $L < $N
+        - pattern: List.length $L <= $N
+      - metavariable-pattern:
+          metavariable: $N
+          patterns:
+            - pattern-not: "0" # covered by list-length-compare-0
+            - pattern-not: List.length ... # covered by list-length-compare-list-length
+    message: computing list length is inefficient for length comparison, use compare_length_with instead
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: list-length-compare-list-length
+    pattern-either:
+      - pattern: List.length $L1 = List.length $L2
+      - pattern: List.length $L1 <> List.length $L2
+      - pattern: List.length $L1 > List.length $L2
+      - pattern: List.length $L1 >= List.length $L2
+      - pattern: List.length $L1 < List.length $L2
+      - pattern: List.length $L1 <= List.length $L2
+    message: computing list length is inefficient for length comparison, use compare_lengths instead
+    languages: [ocaml]
+    severity: WARNING
+
+  - id: list-function-temporary-combine
+    patterns:
+      - pattern: $LF ... (List.combine ... ...)
+      - metavariable-pattern:
+          metavariable: $LF
+          pattern-either:
+            - pattern: List.iter
+            - pattern: List.iteri
+            - pattern: List.map
+            - pattern: List.mapi
+            - pattern: List.rev_map
+            - pattern: List.fold_left
+            - pattern: List.fold_right
+            - pattern: List.for_all
+            - pattern: List.exists
+    message: unnecessary temporary combined list, use 2-suffixed operation directly
+    languages: [ocaml]
+    severity: WARNING

.semgrep/option.yml

@@ -0,0 +1,10 @@
+rules:
+  - id: option-is-some-get
+    patterns:
+      - pattern: Option.get $O
+      - pattern-either:
+        - pattern-inside: if Option.is_some $O then ...
+        - pattern-inside: if ... && Option.is_some $O then ...
+    message: use match instead
+    languages: [ocaml]
+    severity: WARNING

src/analyses/arinc.ml

@@ -163,7 +163,7 @@ struct
       M.debug "mayPointTo: query result for %a is %a" d_exp exp Queries.LS.pretty v;
       (*failwith "mayPointTo"*)
       []
-  let mustPointTo ctx exp = let xs = mayPointTo ctx exp in if List.length xs = 1 then Some (List.hd xs) else None
+  let mustPointTo ctx exp = let xs = mayPointTo ctx exp in if List.compare_length_with xs 1 = 0 then Some (List.hd xs) else None
   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)
 
@@ -224,7 +224,7 @@ struct
                let else_stmts = if List.is_empty bf.bstmts then stmt.succs else bf.bstmts in
                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.length stmt.preds > 1 then ( (* seems like this never happens *)
+               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!";
                    add_edges env ArincUtil.Nop;
                    { ctx.local with pred = Pred.of_node env.node }

src/analyses/base.ml

@@ -218,7 +218,7 @@ struct
                 Some true
               else (
                 (* If the address id definite, it should be one or no variables *)
-                assert (List.length v = 1);
+                assert (List.compare_length_with v 1 = 0);
                 if a.f (Q.IsMultiple (List.hd v)) then
                   None
                 else
@@ -968,14 +968,14 @@ struct
     | Q.EvalStr e -> begin
         match eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         (* exactly one string in the set (works for assignments of string constants) *)
-        | `Address a when List.length (AD.to_string a) = 1 -> (* exactly one string *)
+        | `Address a when List.compare_length_with (AD.to_string a) 1 = 0 -> (* exactly one string *)
           `Lifted (List.hd (AD.to_string a))
         (* check if we have an array of chars that form a string *)
         (* TODO return may-points-to-set of strings *)
-        | `Address a when List.length (AD.to_string a) > 1 -> (* oh oh *)
+        | `Address a when List.compare_length_with (AD.to_string a) 1 > 0 -> (* oh oh *)
           M.debug "EvalStr (%a) returned %a" d_exp e AD.pretty a;
           Queries.Result.top q
-        | `Address a when List.length (AD.to_var_may a) = 1 -> (* some other address *)
+        | `Address a when List.compare_length_with (AD.to_var_may a) 1 = 0 -> (* some other address *)
           (* Cil.varinfo * (AD.Addr.field, AD.Addr.idx) Lval.offs *)
           (* ignore @@ printf "EvalStr `Address: %a -> %s (must %i, may %i)\n" d_plainexp e (VD.short 80 (`Address a)) (List.length @@ AD.to_var_must a) (List.length @@ AD.to_var_may a); *)
           begin match unrollType (Cilfacade.typeOf e) with
@@ -2125,7 +2125,7 @@ struct
       end
     | `Unknown "__builtin" ->
       begin match args with
-        | Const (CStr "invariant") :: args when List.length args > 0 ->
+        | Const (CStr "invariant") :: ((_ :: _) as args) ->
           List.fold_left (fun d e -> invariant ctx (Analyses.ask_of_ctx ctx) ctx.global d e true) ctx.local args
         | _ -> failwith "Unknown __builtin."
       end
@@ -2279,7 +2279,7 @@ struct
       match x.vtype, CPA.find x st.cpa with
       | TPtr (t, attr), `Address a
         when (not (AD.is_top a))
-          && List.length (AD.to_var_may a) = 1
+          && List.compare_length_with (AD.to_var_may a) 1 = 0
           && not (VD.is_immediate_type t)
         ->
         let cv = List.hd (AD.to_var_may a) in

src/analyses/contain.ml

@@ -542,7 +542,7 @@ struct
 
                     let res = List.fold_left (fun y x -> try ignore(Cilfacade.find_varinfo_fundec x);x::y with _ -> y) [] vars in
                     begin
-                      if List.length res = 0 then
+                      if res = [] then
                         begin
                           begin
                             D.report(" (6) unresolved function pointer in "^sprint 160 (d_exp () fval)^" -> "^sprint 160 (ContainDomain.ArgSet.pretty () rvs));

src/analyses/deadlock.ml

@@ -102,7 +102,7 @@ struct
         ) ctx.local (eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist))
       | `Unlock ->
         let lockAddrs = eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist) in
-        if List.length lockAddrs = 1 then
+        if List.compare_length_with lockAddrs 1 = 0 then
           let inLockAddrs e = List.exists (fun r -> ValueDomain.Addr.equal r e.addr) lockAddrs in
           D.filter (neg inLockAddrs) ctx.local
         else ctx.local

src/analyses/extract_arinc.ml

@@ -135,7 +135,7 @@ struct
     let walk_edges (a, out_edges) =
       let edges = Set.elements out_edges |> List.map codegen_edge in
       (label a ^ ":") ::
-      if List.length edges > 1 then
+      if List.compare_length_with edges 1 > 0 then
         "if" :: (choice edges) @ ["fi"]
       else
         edges
@@ -380,7 +380,7 @@ struct
     let mainfuns = GobConfig.get_string_list "mainfun" in
     ignore @@ List.map Pids.get mainfuns;
     ignore @@ List.map (fun name -> Res.get ("process", name)) mainfuns;
-    assert (List.length mainfuns = 1); (* TODO? *)
+    assert (List.compare_length_with mainfuns 1 = 0); (* TODO? *)
     List.iter (fun fname -> Pfuns.add "main" fname) mainfuns;
     if GobConfig.get_bool "ana.arinc.export" then output_file (Goblintutil.create_dir "result/" ^ "arinc.os.pml") (snd (Pml_arinc.init ()))
 

src/analyses/extract_osek.ml

@@ -134,7 +134,7 @@ struct
     let walk_edges (a, out_edges) =
       let edges = Set.elements out_edges |> List.map codegen_edge in
       (label a ^ ":") ::
-      if List.length edges > 1 then
+      if List.compare_length_with edges 1 > 0 then
         "if" :: (choice edges) @ ["fi"]
       else
         edges
@@ -327,7 +327,7 @@ struct
     let mainfuns = GobConfig.get_string_list "mainfun" in
     ignore @@ List.map Pids.get mainfuns;
     ignore @@ List.map (fun name -> Res.get ("process", name)) mainfuns;
-    assert (List.length mainfuns = 1); (* TODO? *)
+    assert (List.compare_length_with mainfuns 1 = 0); (* TODO? *)
     List.iter (fun fname -> Pfuns.add "main" fname) mainfuns;
     output_file (Goblintutil.create_dir "result/" ^ "osek.os.pml") (snd (Pml_osek.init ()))
 

src/analyses/fileUse.ml

@@ -218,8 +218,8 @@ struct
     (* fold possible keys on domain *)
     let ret_all f lval =
       let xs = D.keys_from_lval lval (Analyses.ask_of_ctx ctx) in (* get all possible keys for a given lval *)
-      if List.length xs = 0 then (D.warn @@ "could not resolve "^sprint d_exp (Lval lval); m)
-      else if List.length xs = 1 then f (List.hd xs) m true
+      if xs = [] then (D.warn @@ "could not resolve "^sprint d_exp (Lval lval); m)
+      else if List.compare_length_with xs 1 = 0 then f (List.hd xs) m true
       (* else List.fold_left (fun m k -> D.join m (f k m)) m xs *)
       else
         (* if there is more than one key, join all values and do warnings on the result *)

src/analyses/osek.ml

@@ -639,14 +639,14 @@ struct
         let to_accs (v,o) xs =
           Concrete (Some (Lval lv), v, Offs.from_offset (conv_offset o), write) :: xs
         in
-        if List.length regs = 0 then begin
+        if regs = [] then begin
           if Queries.LS.mem (dummyFunDec.svar,`NoOffset) a
           then [Unknown (Lval lv,write)]
                @ Queries.LS.fold to_accs (Queries.LS.remove (dummyFunDec.svar,`NoOffset) a) []
           else Queries.LS.fold to_accs a []
         end else List.map add_reg regs
       | _ ->
-        if List.length regs = 0
+        if regs = []
         then [Unknown (Lval lv,write)]
         else List.map add_reg regs
 

src/analyses/shapes.ml

@@ -78,7 +78,7 @@ struct
       let (nsm,nds,rmd) = sync_one ask gl upd sm in
       let add_regmap (ls,gs) (rm,part) =
         let set =
-          if List.length gs = 0 then RS.singleton VFB.bullet else
+          if gs = [] then RS.singleton VFB.bullet else
             List.fold_right (fun x -> RS.add (VFB.of_vf (x,[]))) gs (RS.empty ())
         in
         let write_map l rm =

src/analyses/spec.ml

@@ -61,8 +61,7 @@ struct
         if not change_state then m
         else if may then D.may_goto key loc state m else D.goto key loc state m
 
-    (* match spec_exp, cil_exp *)
-    let equal_exp ctx = function
+    let equal_exp ctx spec_exp cil_exp = match spec_exp, cil_exp with
       (* TODO match constants right away to avoid queries? *)
       | `String a, Const(CStr b) -> M.debug "EQUAL String Const: %s = %s" a b; a=b
       (* | `String a, Const(CWStr xs as c) -> failwith "not implemented" *)
@@ -130,7 +129,7 @@ struct
           (* everything matches the constraint -> go to new state and increase counter *)
           else
             (* TODO if #Queries.MayPointTo > 1: each result is May, but all combined are Must *)
-            let may = (List.length keys > 1) in
+            let may = (List.compare_length_with keys 1 > 0) in
             (* do not change state for reflexive edges where the key is not assigned to (e.g. *$p = _) *)
             let change_state = not (old_a=b && SC.get_lval c <> Some `Var) in
             M.debug "GOTO ~may:%B ~change_state:%B. %s -> %s: %s" may change_state a b (SC.stmt_to_string c);
@@ -228,9 +227,9 @@ struct
       SC.equal_form (Some lval) c &&
       (* check for constraints *p = _ where p is the key *)
       match lval, SC.get_lval c with
-      | (Mem Lval x, o), Some `Ptr  when SpecCheck.equal_exp ctx (SC.get_rval c, rval) ->
+      | (Mem Lval x, o), Some `Ptr  when SpecCheck.equal_exp ctx (SC.get_rval c) rval ->
         let keys = D.keys_from_lval x (Analyses.ask_of_ctx ctx) in
-        if List.length keys <> 1 then failwith "not implemented"
+        if List.compare_length_with keys 1 <> 0 then failwith "not implemented"
         else true
       | _ -> false (* nothing to do *)
     in
@@ -332,14 +331,14 @@ struct
           (* filter those edges that are branches, start with a state from states and have the same branch expression and the same tv *)
           let branch_edges = List.filter (fun (a,ws,fwd,b,c) -> SC.is_branch c && List.mem a states && branch_exp_eq c exp tv) !edges in
           (* there should be only one such edge or none *)
-          if List.length branch_edges <> 1 then ( (* call of branch for an actual branch *)
+          if List.compare_length_with branch_edges 1 <> 0 then ( (* call of branch for an actual branch *)
             M.debug "branch: branch_edges length is not 1! -> actual branch";
             M.debug "%s -> branch_edges1: %a" (D.string_of_entry key m) (Pretty.d_list "\n " (fun () x -> Pretty.text (SC.def_to_string (SC.Edge x)))) branch_edges;
             (* filter those edges that are branches, end with a state from states have the same branch expression and the same tv *)
             (* TODO they should end with any predecessor of the current state, not only the direct predecessor *)
             let branch_edges = List.filter (fun (a,ws,fwd,b,c) -> SC.is_branch c && List.mem b states && branch_exp_eq c exp tv) !edges in
             M.debug "%s -> branch_edges2: %a" (D.string_of_entry key m) (Pretty.d_list "\n " (fun () x -> Pretty.text (SC.def_to_string (SC.Edge x)))) branch_edges;
-            if List.length branch_edges <> 1 then m else
+            if List.compare_length_with branch_edges 1 <> 0 then m else
               (* meet current value with the target state. this is tricky: we can not simply take the target state, since there might have been more than one element already before the branching.
                  -> find out what the alternative branch target was and remove it *)
               let (a,ws,fwd,b,c) = List.hd branch_edges in
@@ -471,13 +470,13 @@ struct
     in
     let matches (a,ws,fwd,b,c) =
       let equal_args spec_args cil_args =
-        if List.length spec_args = 1 && List.hd spec_args = `Free then
+        if List.compare_length_with spec_args 1 = 0 && List.hd spec_args = `Free then
           true (* wildcard as an argument matches everything *)
-        else if List.length arglist <> List.length spec_args then (
+        else if List.compare_lengths arglist spec_args <> 0 then (
           M.debug "SKIP the number of arguments doesn't match the specification!";
           false
         )else
-          List.for_all (SpecCheck.equal_exp ctx) (List.combine spec_args cil_args) (* TODO Cil.constFold true arg. Test: Spec and c-file: 1+1 *)
+          List.for_all2 (SpecCheck.equal_exp ctx) spec_args cil_args (* TODO Cil.constFold true arg. Test: Spec and c-file: 1+1 *)
       in
       (* function name must fit the constraint *)
       SC.fname_is f.vname c &&

src/cdomains/fileDomain.ml

@@ -49,8 +49,8 @@ struct
     let must_true = BatList.filter_map (f (`Must true)) xs in
     let may_true  = BatList.filter_map (f (`May true)) xs in
     (* output first must and first may *)
-    if List.length must_true > 0 then (List.hd must_true) ();
-    if List.length may_true  > 0 then (List.hd may_true) ()
+    if must_true <> [] then (List.hd must_true) ();
+    if may_true <> [] then (List.hd may_true) ()
 
   (* handling state *)
   let opened   r = V.state r |> Val.opened

src/cdomains/stackDomain.ml

@@ -37,7 +37,7 @@ struct
   let bot () : t = times (Var.bot ()) n
 
   let leq (x:t) (y:t) =
-    if List.length x < List.length y then false else
+    if List.compare_lengths x y < 0 then false else
       let f acc x y = Var.leq x y && acc in
       fold_left2 f true false x y
 

src/cdomains/valueDomain.ml

@@ -412,7 +412,7 @@ struct
           if ci.cstruct then
             `Struct (match v with
                 | `Struct x when same_struct x -> x
-                | `Struct x when List.length ci.cfields > 0 ->
+                | `Struct x when ci.cfields <> [] ->
                   let first = List.hd ci.cfields in
                   Structs.(replace (top ()) first (get x first))
                 | _ -> log_top __POS__; Structs.top ()

src/domains/octagonMapDomain.ml

@@ -686,7 +686,7 @@ module MapOctagon : S
   let use_matrix_closure = true
 
   let remove_empty = filter (fun var (const, consts) ->
-      not (INV.is_top_of (ikind ()) const) || not ((List.length consts) = 0))
+      not (INV.is_top_of (ikind ()) const) || consts <> [])
 
   let strong_closure oct =
     if use_matrix_closure then

src/domains/printable.ml

@@ -611,7 +611,7 @@ let get_short_list begin_str end_str list =
   let cut_str_list_rev = List.map fst cut_str_pair_list_rev in
 
   let cut_str_list =
-    if ((List.length cut_str_list_rev) < (List.length list)) then
+    if List.compare_lengths cut_str_list_rev list < 0 then
       List.rev (continues::cut_str_list_rev)
     else
       List.rev cut_str_list_rev in

src/extract/pml.ml

@@ -90,10 +90,10 @@ let nop = (), ""
 module Chan = struct (* channels *)
   let create len content = Chan { capacity = len; content = []; content_type = content }
 
-  let full   (c,s) = List.length c.content >= fst c.capacity, "full("^s^")"
-  let nfull  (c,s) = List.length c.content < fst c.capacity, "nfull("^s^")"
-  let empty  (c,s) = List.length c.content = 0, "empty("^s^")"
-  let nempty (c,s) = List.length c.content > 0, "nempty("^s^")"
+  let full   (c,s) = List.compare_length_with c.content (fst c.capacity) >= 0, "full("^s^")"
+  let nfull  (c,s) = List.compare_length_with c.content (fst c.capacity) < 0, "nfull("^s^")"
+  let empty  (c,s) = c.content = [], "empty("^s^")"
+  let nempty (c,s) = c.content <> [], "nempty("^s^")"
   let len    (c,s) = List.length c.content, "len("^s^")"
 
   (*  ? = first, ?? = any, no <> = consume, <> = remain, TODO eval, !! *)
@@ -126,7 +126,7 @@ let indent x = String.split_on_string "\n" x |> List.map (fun x -> "  "^x) |> St
 
 let surround a b (v,s) = v, a^"\n"^indent s^"\n"^b
 let _match xs =
-  assert (List.length xs > 0);
+  assert (xs <> []);
   let s = String.concat "\n" @@ List.map (fun (c,b) -> ":: "^snd c^" -> "^snd b) xs in
   (*List.find (fst%fst) xs, s*)
   (), s

src/framework/cfgTools.ml

@@ -468,9 +468,9 @@ let createCFG (file: file) =
 let minimizeCFG (fw,bw) =
   let keep = H.create 113 in
   let comp_keep t (_,f) =
-    if (List.length (H.find_all bw t)<>1) || (List.length (H.find_all fw t)<>1) then
+    if (List.compare_length_with (H.find_all bw t) 1 <> 0) || (List.compare_length_with (H.find_all fw t) 1 <> 0) then
       H.replace keep t ();
-    if (List.length (H.find_all bw f)<>1) || (List.length (H.find_all fw f)<>1) then
+    if (List.compare_length_with (H.find_all bw f) 1 <> 0) || (List.compare_length_with (H.find_all fw f) 1 <> 0) then
       H.replace keep f ()
   in
   H.iter comp_keep bw;

src/framework/control.ml

@@ -533,7 +533,7 @@ struct
 
       (* run activated transformations with the analysis result *)
       let active_transformations = get_string_list "trans.activated" in
-      (if List.length active_transformations > 0 then
+      (if active_transformations <> [] then
         (* Transformations work using Cil visitors which use the location, so we join all contexts per location. *)
         let joined =
           let open Batteries in let open Enum in