Adapt to new CIL with CInt instead of CInt64

goblint.opam

@@ -58,7 +58,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9ad7b51e362a2fa6fefb706e4ebc95c708f251f5" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

goblint.opam.locked

@@ -94,7 +94,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b"
+    "git+https://github.com/goblint/cil.git#9ad7b51e362a2fa6fefb706e4ebc95c708f251f5"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9ad7b51e362a2fa6fefb706e4ebc95c708f251f5" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

src/analyses/arinc.ml

@@ -136,7 +136,7 @@ struct
   let is_return_code_type exp = Cilfacade.typeOf exp |> unrollTypeDeep |> function
     | TEnum(ei, _) when ei.ename = "T13" -> true
     | _ -> false
-  let return_code_is_success = function 0L | 1L -> true | _ -> false
+  let return_code_is_success z = Cilint.is_zero_cilint z || Cilint.compare_cilint z Cilint.one_cilint = 0
   let str_return_code i = if return_code_is_success i then "SUCCESS" else "ERROR"
   let str_return_dlval (v,o as dlval) =
     sprint d_lval (Lval.CilLval.to_lval dlval) ^ "_" ^ string_of_int v.vdecl.line |>
@@ -195,7 +195,7 @@ struct
               let add_one str_rhs = add_edges env @@ ArincUtil.Assign (str_return_dlval dlval, str_rhs) in
               let add_top () = add_edges ~r:(str_return_dlval dlval) env @@ ArincUtil.Nop in
               match stripCasts rval with
-              | Const CInt64(i,_,_) -> add_one @@ str_return_code i
+              | Const CInt(i,_,_) -> add_one @@ str_return_code i
               (*       | Lval rlval ->
                         iterMayPointTo ctx (AddrOf rlval) (fun rdlval -> add_return_dlval env `Read rdlval; add_one @@ str_return_dlval rdlval) *)
               | _ -> add_top ()
@@ -212,8 +212,8 @@ struct
         let check a b tv =
           (* we are interested in a comparison between some lval lval (which has the type of the return code enum) and a value of that enum (which gets converted to an Int by CIL) *)
           match a, b with
-          | Lval lval, Const CInt64(i,_,_)
-          | Const CInt64(i,_,_), Lval lval when is_return_code_type (Lval lval) ->
+          | Lval lval, Const CInt(i,_,_)
+          | Const CInt(i,_,_), Lval lval when is_return_code_type (Lval lval) ->
             (* let success = return_code_is_success i = tv in (* both must be true or false *) *)
             (* ignore(printf "if %s: %a = %B (line %i)\n" (if success then "success" else "error") d_plainexp exp tv (!Tracing.current_loc).line); *)
             (match env.node with

src/analyses/base.ml

@@ -486,12 +486,10 @@ struct
 
   let convertToQueryLval x =
     let rec offsNormal o =
+      let ik = Cilfacade.ptrdiff_ikind () in
       let toInt i =
-        match IdxDom.to_int i with
-        | Some x ->
-          (* TODO: Handle values outside of int64 *)
-          let x = BI.to_int64 x in
-          Const (CInt64 (x,IInt, None))
+        match IdxDom.to_int @@ ID.cast_to ik i with
+        | Some x -> Const (CInt (x,ik, None))
         | _ -> mkCast (Const (CStr "unknown")) intType
 
       in
@@ -667,10 +665,10 @@ struct
       (* query functions were no help ... now try with values*)
       match (if get_bool "exp.lower-constants" then constFold true exp else exp) with
       (* Integer literals *)
-      (* seems like constFold already converts CChr to CInt64 *)
+      (* seems like constFold already converts CChr to CInt *)
       | Const (CChr x) -> eval_rv a gs st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
-      | Const (CInt64 (num,ikind,str)) ->
-        (match str with Some x -> M.tracel "casto" "CInt64 (%s, %a, %s)\n" (Int64.to_string num) d_ikind ikind x | None -> ());
+      | Const (CInt (num,ikind,str)) ->
+        (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Cilint.string_of_cilint num) d_ikind ikind x | None -> ());
         `Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
       (* String literals *)
       | Const (CStr x) -> `Address (AD.from_string x) (* normal 8-bit strings, type: char* *)
@@ -700,8 +698,8 @@ struct
           let cast_ok = function
             | Addr a ->
               begin
-                match Cil.isInteger (sizeOf t), Cil.isInteger (sizeOf (get_type_addr a)) with
-                | Some i1, Some i2 -> Int64.compare i1 i2 <= 0
+                match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf (get_type_addr a)) with
+                | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0
                 | _ ->
                   if contains_vla t || contains_vla (get_type_addr a) then
                     begin
@@ -1665,7 +1663,7 @@ struct
     let lval_t = Cilfacade.typeOf rval in
     let char_array_hack () =
       let rec split_offset = function
-        | Index(Const(CInt64(i, _, _)), NoOffset) -> (* ...[i] *)
+        | Index(Const(CInt(i, _, _)), NoOffset) -> (* ...[i] *)
           Index(zero, NoOffset), Some i (* all i point to StartOf(string) *)
         | NoOffset -> NoOffset, None
         | Index(exp, offs) ->
@@ -1682,7 +1680,7 @@ struct
       in
       match last_index lval, stripCasts rval with
       | Some (lv, i), Const(CChr c) when c<>'\000' -> (* "abc" <> "abc\000" in OCaml! *)
-        let i = i64_to_int i in
+        let i = Cilint.int_of_cilint i in
         (* ignore @@ printf "%a[%i] = %c\n" d_lval lv i c; *)
         let s = try Hashtbl.find char_array lv with Not_found -> Bytes.empty in (* current string for lv or empty string *)
         if i >= Bytes.length s then ((* optimized b/c Out_of_memory *)

src/analyses/deadlock.ml

@@ -79,7 +79,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
+    | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
     | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 

src/analyses/expRelation.ml

@@ -4,6 +4,7 @@
 
 open Prelude.Ana
 open Analyses
+open Cilint
 
 module Spec : Analyses.MCPSpec =
 struct
@@ -58,25 +59,26 @@ struct
       Basetype.CilExp.equal (canonize e1) (canonize e2)
     | Queries.MayBeLess (e1, e2) when not (isFloat e1) ->
       begin
+        (* Compare the cilint first in the hope that it is cheaper than the LVal comparison *)
         match e1, e2 with
-        | BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2 when (lvalsEq l1 l2 && Int64.compare i Int64.zero > 0) ->
+        | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (compare_cilint i zero_cilint > 0 && lvalsEq l1 l2) ->
             false  (* c > 0 => (! x+c < x) *)
-        | Lval l1, BinOp(PlusA, Lval l2, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2 && Int64.compare i Int64.zero < 0) ->
+        | Lval l1, BinOp(PlusA, Lval l2, Const(CInt(i,_,_)), _) when (compare_cilint i zero_cilint < 0 && lvalsEq l1 l2) ->
             false  (* c < 0 => (! x < x+c )*)
-        | BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2 when (lvalsEq l1 l2 && Int64.compare i Int64.zero < 0) ->
+        | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (compare_cilint i zero_cilint < 0 && lvalsEq l1 l2) ->
             false  (* c < 0 => (! x-c < x) *)
-        | Lval l1, BinOp(MinusA, Lval l2, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2 && Int64.compare i Int64.zero > 0) ->
+        | Lval l1, BinOp(MinusA, Lval l2, Const(CInt(i,_,_)), _) when (compare_cilint i zero_cilint > 0 && lvalsEq l1 l2) ->
             false  (* c < 0 => (! x < x-c) *)
         | _ ->
             true
       end
     | Queries.MayBeEqual (e1,e2) when not (isFloat e1) ->
       begin
         match e1,e2 with
-        | BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2
-        | Lval l2, BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _)
-        | BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2
-        | Lval l2, BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2) && Int64.compare i Int64.zero <> 0  ->
+        | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2
+        | Lval l2, BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _)
+        | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2
+        | Lval l2, BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _) when compare_cilint i zero_cilint <> 0 && (lvalsEq l1 l2) ->
             false
         | _ -> true
       end

src/analyses/fileUse.ml

@@ -89,11 +89,11 @@ struct
     let check a b tv =
       (* ignore(printf "check: %a = %a, %B\n" d_plainexp a d_plainexp b tv); *)
       match a, b with
-      | Const (CInt64(i, kind, str)), Lval lval
-      | Lval lval, Const (CInt64(i, kind, str)) ->
+      | Const (CInt(i, kind, str)), Lval lval
+      | Lval lval, Const (CInt(i, kind, str)) ->
         (* ignore(printf "branch(%s==%i, %B)\n" v.vname (Int64.to_int i) tv); *)
         let k = D.key_from_lval lval in
-        if i = Int64.zero && tv then (
+        if Cilint.compare_cilint i Cilint.zero_cilint = 0 && tv then (
           (* ignore(printf "error-branch\n"); *)
           D.error k m
         )else

src/analyses/flag.ml

@@ -55,14 +55,14 @@ struct
           let x = var.vname in if List.mem x !noflags then () else
             (* let _ = print_endline ( List.fold_left (fun acc a -> a ^ ", " ^ acc) "" !flags   ) in  *)
             (match rval with
-             | Const (CInt64 (i,_,_)) -> if List.mem x !flags then
+             | Const (CInt(i,_,_)) -> if List.mem x !flags then
                  let v = Hashtbl.find vars x in
                  (* let _ = print_endline ( "assign" ^ (Int64.to_string i)) in   *)
                  (* let _ = print_endline ( x ^ " has values " ^ VSet.fold (fun e str -> (Val.short 50 e) ^", " ^str  ) v " ") in       *)
-                 if (VSet.mem (Val.of_int i) v) then () else
+                 if (VSet.mem (Val.of_int (Cilint.int64_of_cilint i)) v) then () else (* dubious, but was already like this *)
                  if (VSet.cardinal v < flagmax) then
                    (* let _ = print_endline ( "add") in   *)
-                   Hashtbl.replace vars x (VSet.add (Val.of_int i) v)
+                   Hashtbl.replace vars x (VSet.add (Val.of_int (Cilint.int64_of_cilint i)) v) (* dubious, but was already like this *)
                  else begin
                    (* let _ = print_endline ( "remove") in   *)
                    flags := listrem x !flags;
@@ -72,7 +72,7 @@ struct
                  end
                else begin
                  flags := x ::!flags;
-                 Hashtbl.add vars x (VSet.add (Val.of_int i) (VSet.empty ()) )
+                 Hashtbl.add vars x (VSet.add (Val.of_int (Cilint.int64_of_cilint i)) (VSet.empty ())) (* dubious, but was already like this *)
                end
              | _ ->
                noflags := x::!noflags; if List.mem x !flags then begin

src/analyses/malloc_null.ml

@@ -24,7 +24,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
+    | `Index (Const (CInt (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
     | `Index (_,o) -> `Index (IdxDom.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 

src/analyses/mayLocks.ml

@@ -24,7 +24,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
+    | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
     | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 

src/analyses/mutexAnalysis.ml

@@ -50,7 +50,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_offset o)
+    | `Index (Const (CInt (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_offset o)
     | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 
@@ -63,7 +63,7 @@ struct
   let rec conv_const_offset x =
     match x with
     | NoOffset    -> `NoOffset
-    | Index (Const (CInt64 (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_const_offset o)
+    | Index (Const (CInt (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_const_offset o)
     | Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_const_offset o)
     | Field (f,o) -> `Field (f, conv_const_offset o)
 

src/analyses/octagon.ml

@@ -36,20 +36,19 @@ struct
 
   let evaluate_sums oct exp =
     let match_exp = function
-      | BinOp(Mult, Lval(Var(var), _), Const(CInt64 (c, _, _)), _)
-      | BinOp(Mult, Const(CInt64 (c, _, _)), Lval(Var(var), NoOffset), _) ->
+      | BinOp(Mult, Lval(Var(var), _), Const(CInt (c, _, _)), _)
+      | BinOp(Mult, Const(CInt (c, _, _)), Lval(Var(var), NoOffset), _) ->
         Some (c, var)
       | Lval(Var(var), NoOffset) ->
-        Some (Int64.one, var)
+        Some (Cilint.one_cilint, var)
       | _ -> None
     in
 
     match exp with
     | BinOp(op, expl, expr, _) when op = PlusA || op = MinusA ->
       begin match match_exp expl, match_exp expr with
         | Some(cl, varl), Some(cr, varr) when (BV.compare varl varr <> 0) -> (* this is needed as projection with varl=varr throws an exception (?) *)
-          let cr = if op = PlusA then cr else Int64.neg cr in
-          let cl, cr = Tuple2.mapn BI.of_int64 (cl, cr) in
+          let cr = if op = PlusA then cr else Cilint.neg_cilint cr in
           let cl, cr = INV.of_int oct_ik cl, INV.of_int oct_ik cr in
           let varSum = D.projection varl (Some (true, varr)) oct in
           let varDif1 = D.projection varl (Some (false, varr)) oct in
@@ -74,7 +73,7 @@ struct
     | None ->
       begin
         match exp with
-        | Const (CInt64 (i, _, _)) -> INV.of_int oct_ik (BI.of_int64 i)
+        | Const (CInt (i, _, _)) -> INV.of_int oct_ik i
         | Lval (Var var, NoOffset) -> D.projection var None oct
         | UnOp (Neg, exp, _) ->
           INV.neg (evaluate_exp oct exp)
@@ -116,19 +115,19 @@ struct
               D.set_constraint (var1, Some(ConstraintType.minus, v), CT.UpperAndLower, i) oct, true (* TODO: Is this ok, we need to be careful when to do closures *)
          in
          (match rval with
-          | BinOp(op, Lval(Var(var), NoOffset), Const(CInt64 (integer, _, _)), _)
+          | BinOp(op, Lval(Var(var), NoOffset), Const(CInt (integer, _, _)), _)
             when (op = PlusA || op = MinusA) && is_local_and_not_pointed_to var ->
             begin
-              let integer = BI.of_int64 @@
+              let integer =
                 if op = MinusA then
-                  Int64.neg integer
+                  Cilint.neg_cilint integer
                 else
                   integer
               in
               assignVarPlusInt var integer
             end
-          | BinOp(PlusA, Const(CInt64 (integer, _, _)), Lval(Var(var), NoOffset), _) when is_local_and_not_pointed_to var ->
-            assignVarPlusInt var (BI.of_int64 integer)
+          | BinOp(PlusA, Const(CInt (integer, _, _)), Lval(Var(var), NoOffset), _) when is_local_and_not_pointed_to var ->
+            assignVarPlusInt var integer
           | Lval(Var var, NoOffset) when is_local_and_not_pointed_to var ->
             assignVarPlusInt var BI.zero
           | exp ->
@@ -304,26 +303,26 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     let rec getSumAndDiffForVars exp1 exp2 =
-      let addConstant x c = BatOption.map (OctagonDomain.INV.add (OctagonDomain.INV.of_int oct_ik (BI.of_int64 c))) x in
+      let addConstant x c = BatOption.map (OctagonDomain.INV.add (OctagonDomain.INV.of_int oct_ik c)) x in
       match exp1, exp2 with
-      | BinOp(PlusA, Lval l1, Const(CInt64(c,_,_)), _), Lval l2 ->
+      | BinOp(PlusA, Lval l1, Const(CInt(c,_,_)), _), Lval l2 ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
         addConstant sum c, addConstant diff c                         (* a+c <= (x+c)-y <= b+c (add c to all sides)    *)
-      | Lval l1, BinOp(PlusA, Lval l2, Const(CInt64(c,_,_)), _) ->
+      | Lval l1, BinOp(PlusA, Lval l2, Const(CInt(c,_,_)), _) ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
-        addConstant sum (Int64.neg c), addConstant diff (Int64.neg c) (* x-(y+c)= x-y-c --> a-c <= x-(y+c) <= b-c      *)
-      | BinOp(MinusA, Lval l1, Const(CInt64(c,_,_)), _), Lval l2 ->
+        addConstant sum (Cilint.neg_cilint c), addConstant diff (Cilint.neg_cilint c) (* x-(y+c)= x-y-c --> a-c <= x-(y+c) <= b-c      *)
+      | BinOp(MinusA, Lval l1, Const(CInt(c,_,_)), _), Lval l2 ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
-        addConstant sum (Int64.neg c), addConstant diff (Int64.neg c) (* (x-c)-y = x-y-c --> a-c <= (x-c)-y <= b-c     *)
-      | Lval l1, BinOp(MinusA, Lval l2, Const(CInt64(c,_,_)), _) ->
+        addConstant sum (Cilint.neg_cilint c), addConstant diff (Cilint.neg_cilint c) (* (x-c)-y = x-y-c --> a-c <= (x-c)-y <= b-c     *)
+      | Lval l1, BinOp(MinusA, Lval l2, Const(CInt(c,_,_)), _) ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
         addConstant sum c, addConstant diff c                         (* x-(y-c) = x-y+c --> a+c <= x-(y-c) <= b+c     *)
       | Lval(Var v1, NoOffset), Lval(Var v2, NoOffset) ->
         let sum, diff, flag = D.get_relation v1 v2 ctx.local in
         if not flag then
           sum, diff
         else
-          sum, BatOption.map (OctagonDomain.INV.mul (INV.of_int oct_ik (BI.of_int64 Int64.minus_one))) diff
+          sum, BatOption.map (OctagonDomain.INV.mul (INV.of_int oct_ik Cilint.mone_cilint)) diff
       | _ -> None, None
     in
     match q with