Merge pull request #479 from goblint/no_cilint

Adapt to new CIL with CInt instead of CInt64

Author: michael-schwarz

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#64f3010e56563cf78ab3f4535b8614ef8f4e3abf" ]
   # 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#64f3010e56563cf78ab3f4535b8614ef8f4e3abf"
   ]
   [
     "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#64f3010e56563cf78ab3f4535b8614ef8f4e3abf" ]
   # 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

@@ -509,12 +509,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
@@ -690,10 +688,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* *)
@@ -723,8 +721,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
@@ -1689,7 +1687,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) ->
@@ -1706,7 +1704,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

@@ -78,7 +78,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
@@ -57,25 +58,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

@@ -88,11 +88,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

@@ -54,14 +54,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;
@@ -71,7 +71,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

@@ -23,7 +23,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)