Merge pull request #1851 from goblint/semgrep-cil-var

Use `GoblintCil.var` where possible

Author: sim642

.semgrep/cil.yml

@@ -15,3 +15,11 @@ rules:
     message: use Cilfacade instead
     languages: [ocaml]
     severity: WARNING
+
+  - id: cil-var
+    pattern: (Var $X, NoOffset)
+    # Autofix is broken: https://github.com/semgrep/semgrep/issues/11278
+    # fix: GoblintCil.var $X
+    message: use GoblintCil.var instead
+    languages: [ocaml]
+    severity: WARNING

src/analyses/apron/relationAnalysis.apron.ml

@@ -506,7 +506,7 @@ struct
         foldGlobals !Cilfacade.current_file (fun acc global ->
             match global with
             | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-              mkAddrOf (Var vi, NoOffset) :: acc
+              mkAddrOf (Cil.var vi) :: acc
             (* TODO: what about GVarDecl? *)
             | _ -> acc
           ) deep_addrs

src/analyses/base.ml

@@ -2058,7 +2058,7 @@ struct
     if not (Cil.isArrayType v.vtype) then
       man.local
     else
-      let lval = eval_lv ~man man.local (Var v, NoOffset) in
+      let lval = eval_lv ~man man.local (Cil.var v) in
       let current_value = eval_rv ~man man.local (Lval (Var v, NoOffset)) in
       let new_value = VD.update_array_lengths (eval_rv ~man man.local) current_value v.vtype in
       set ~man man.local lval v.vtype new_value
@@ -2233,7 +2233,7 @@ struct
         foldGlobals !Cilfacade.current_file (fun acc global ->
             match global with
             | GVar (vi, _, _) when not (is_static vi) ->
-              mkAddrOf (Var vi, NoOffset) :: acc
+              mkAddrOf (Cil.var vi) :: acc
             (* TODO: what about GVarDecl? *)
             | _ -> acc
           ) deep_addrs

src/analyses/baseInvariant.ml

@@ -107,7 +107,7 @@ struct
       if is_some_bot v then contra st
       else (
         if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)" CilType.Varinfo.pretty var VD.pretty old_val VD.pretty v pretty c VD.pretty c';
-        let r = set' (Var var,NoOffset) v st in
+        let r = set' (Cil.var var) v st in
         if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r;
         r
       )

src/analyses/c2poAnalysis.ml

@@ -247,7 +247,7 @@ struct
       let state_with_ghosts = meet_conjs_opt equalities_to_add d.data in
       let state_with_ghosts = data_to_t state_with_ghosts in
       if M.tracing then begin
-        let dummy_lval = Var (Var.dummy_varinfo (TVoid [])), NoOffset in
+        let dummy_lval = Cil.var (Var.dummy_varinfo (TVoid [])) in
         let lval = BatOption.default dummy_lval var_opt in
         M.trace "c2po-function" "enter1: var_opt: %a; state: %s; state_with_ghosts: %s\n" d_lval lval (D.show ctx.local) (C2PODomain.show state_with_ghosts);
       end;
@@ -295,7 +295,7 @@ struct
         let cc = remove_out_of_scope_vars d.data f in
         let d = data_to_t cc in
         if M.tracing then begin
-          let dummy_lval = Var (Var.dummy_varinfo (TVoid[])), NoOffset in
+          let dummy_lval = Cil.var (Var.dummy_varinfo (TVoid[])) in
           let lval = BatOption.default dummy_lval lval_opt in
           M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d)
         end;

src/analyses/startStateAnalysis.ml

@@ -55,7 +55,7 @@ struct
       let lval = Lval (Var var, NoOffset) in
       let value = get_value (ask_of_man ctx) lval in
       let duplicated_var = to_varinfo (DuplicVar var) in
-      if M.tracing then M.trace "startState" "added value: var: %a; value: %a" d_lval (Var duplicated_var, NoOffset) AD.pretty value;
+      if M.tracing then M.trace "startState" "added value: var: %a; value: %a" CilType.Varinfo.pretty duplicated_var AD.pretty value;
       D.add duplicated_var value st
     in
     (* assign function parameters *)

src/analyses/taintPartialContexts.ml

@@ -68,7 +68,7 @@ struct
         foldGlobals !Cilfacade.current_file (fun acc global ->
             match global with
             | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-              mkAddrOf (Var vi, NoOffset) :: acc
+              mkAddrOf (Cil.var vi) :: acc
             (* TODO: what about GVarDecl? (see "base.ml -> special_unknown_invalidate")*)
             | _ -> acc
           ) deep_addrs

src/analyses/varEq.ml

@@ -411,7 +411,7 @@ struct
 
   (* Just remove things that go out of scope. *)
   let return man exp fundec  =
-    let rm acc v = remove (Analyses.ask_of_man man) (Var v, NoOffset) acc in
+    let rm acc v = remove (Analyses.ask_of_man man) (Cil.var v) acc in
     List.fold_left rm man.local (fundec.sformals@fundec.slocals)
 
   (* removes all equalities with lval and then tries to make a new one: lval=rval *)
@@ -427,9 +427,9 @@ struct
       | x::xs, y::ys -> fold_left2 f (f r x y) xs ys
       | _ -> r
     in
-    let assign_one_param st lv exp =
-      let rm = remove (Analyses.ask_of_man man) (Var lv, NoOffset) st in
-      add_eq (Analyses.ask_of_man man) (Var lv, NoOffset) exp rm
+    let assign_one_param st v exp =
+      let rm = remove (Analyses.ask_of_man man) (Cil.var v) st in
+      add_eq (Analyses.ask_of_man man) (Cil.var v) exp rm
     in
     let nst =
       try fold_left2 assign_one_param man.local f.sformals args

src/cdomains/unionFind.ml

@@ -320,7 +320,7 @@ module T = struct
     function
     | Addr v ->
       let varinfo = Var.to_varinfo v in
-      let lval = (Var varinfo, NoOffset) in
+      let lval = Cil.var varinfo in
       AddrOf lval
     | Aux (_, exp)
     | (Deref (_, _, exp)) -> exp

src/util/returnUtil.ml

@@ -6,6 +6,6 @@ module AD = ValueDomain.AD
 let return_varstore = ref dummyFunDec.svar
 let return_varinfo () = !return_varstore
 let return_var () = AD.of_var (return_varinfo ())
-let return_lval (): lval = (Var (return_varinfo ()), NoOffset)
+let return_lval (): lval = Cil.var (return_varinfo ())
 
 let longjmp_return = ref dummyFunDec.svar