Merge pull request #1894 from goblint/cast-kind

Add cast kinds in CIL

Author: sim642

goblint.opam

@@ -102,7 +102,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

goblint.opam.locked

@@ -148,7 +148,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.9"
-    "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e"
+    "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712"
   ]
   [
     "apron.v0.9.15"

goblint.opam.template

@@ -3,7 +3,7 @@
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#e21285af8f4408ed5354b1674dab840c43e84712" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

src/analyses/apron/relationAnalysis.apron.ml

@@ -216,7 +216,7 @@ struct
       | Const x -> e
       | UnOp (unop, e, typ) -> UnOp(unop, inner e, typ)
       | BinOp (binop, e1, e2, typ) -> BinOp (binop, inner e1, inner e2, typ)
-      | CastE (t,e) -> CastE (t, inner e)
+      | CastE (k,t,e) -> CastE (k, t, inner e)
       | Lval (Var v, off) -> Lval (Var v, off)
       | Lval (Mem e, NoOffset) ->
         begin match ask (Queries.MayPointTo e) with

src/analyses/base.ml

@@ -825,7 +825,7 @@ struct
         eval_rv_base_lval ~eval_lv ~man st exp lv
       (* Binary operators *)
       (* Eq/Ne when both values are equal and casted to the same type *)
-      | BinOp ((Eq | Ne) as op, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
+      | BinOp ((Eq | Ne) as op, (CastE (_, t1, e1) as c1), (CastE (_, t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
         let a1 = eval_rv ~man st e1 in
         let a2 = eval_rv ~man st e2 in
         let extra_is_safe =
@@ -842,7 +842,7 @@ struct
         (* split nested LOr Eqs to equality pairs, if possible *)
         let rec split = function
           (* copied from above to support pointer equalities with implicit casts inserted *)
-          | BinOp (Eq, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
+          | BinOp (Eq, (CastE (_, t1, e1) as c1), (CastE (_, t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
             Some [binop_remove_same_casts ~extra_is_safe:false ~e1 ~e2 ~t1 ~t2 ~c1 ~c2]
           | BinOp (Eq, arg1, arg2, _) ->
             Some [(arg1, arg2)]
@@ -927,8 +927,8 @@ struct
         let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
         let array_start = add_offset_varinfo array_ofs in
         Address (AD.map array_start (eval_lv ~man st lval))
-      | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
-      | CastE  (t, exp) ->
+      | CastE (_, t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
+      | CastE (_, t, exp) ->
         (let v = eval_rv ~man st exp in
          try
            VD.cast ~torg:(Cilfacade.typeOf exp) t v
@@ -1072,7 +1072,7 @@ struct
     match ofs with
     | NoOffset -> `NoOffset
     | Field (fld, ofs) -> `Field (fld, convert_offset ~man st ofs)
-    | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
+    | Index (exp, ofs) when Offset.Index.Exp.is_any exp -> (* special offset added by convertToQueryLval *)
       `Index (IdxDom.top (), convert_offset ~man st ofs)
     | Index (exp, ofs) ->
       match eval_rv ~man st exp with
@@ -1395,7 +1395,7 @@ struct
         | Imag e
         | SizeOfE e
         | AlignOfE e
-        | CastE (_, e) -> exp_may_signed_overflow man e
+        | CastE (_, _, e) -> exp_may_signed_overflow man e
         | UnOp (unop, e, _) ->
           (* check if the current operation causes a signed overflow *)
           begin match unop with
@@ -2391,7 +2391,8 @@ struct
                     |> AD.type_of in
       (* when src and destination type coincide, take value from the source, otherwise use top *)
       let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then
-          let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
+          (* TODO: why cast if types coincide? *)
+          let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~kind:Internal ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
           eval_rv ~man st (Lval src_cast_lval)
         else
           VD.top_value (unrollType dest_typ)

src/analyses/baseInvariant.ml

@@ -245,9 +245,9 @@ struct
         else
           `NotUnderstood
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
-      | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
+      | BinOp(op, CastE (_, t1, c1), CastE (_, t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
-      | BinOp(op, CastE (t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
+      | BinOp(op, CastE (_, t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
         begin match eval_rv ~man st (Lval x) with
           | Int v ->
             if VD.is_dynamically_safe_cast t1 (Cilfacade.typeOfLval x) (Int v) then
@@ -256,8 +256,8 @@ struct
               `NotUnderstood
           | _ -> `NotUnderstood
         end
-      | BinOp(op, rval, CastE (ti, Lval x), typ) when Cil.isIntegralType ti ->
-        derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv
+      | BinOp(op, rval, CastE (k, ti, Lval x), typ) when Cil.isIntegralType ti ->
+        derived_invariant (BinOp (switchedOp op, CastE(k, ti, Lval x), rval, typ)) tv
       | BinOp(op, (Const _ | AddrOf _), rval, typ) ->
         (* This is last such that we never reach here with rval being Lval (it is swapped around). *)
         `NothingToRefine
@@ -649,15 +649,15 @@ struct
         | UnOp (Neg, e, _), Float c -> inv_exp (unop_FD Neg c) e st
         | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_statically_safe_cast fails for all float types anyways *)
-        | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) ->
+        | BinOp((Eq | Ne) as op, CastE (_, t1, e1), CastE (_, t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) ->
           inv_exp (Int c) (BinOp (op, e1, e2, t)) st
         | BinOp (LOr, arg1, arg2, typ) as exp, Int c ->
           (* copied & modified from eval_rv_base... *)
           let (let*) = Option.bind in
           (* split nested LOr Eqs to equality pairs, if possible *)
           let rec split = function
             (* copied from above to support pointer equalities with implicit casts inserted *)
-            | BinOp (Eq, CastE (t1, e1), CastE (t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
+            | BinOp (Eq, CastE (_, t1, e1), CastE (_, t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
               Some [(e1, e2)]
             | BinOp (Eq, arg1, arg2, _) ->
               Some [(arg1, arg2)]
@@ -835,7 +835,7 @@ struct
             | _ -> assert false
           end
         | Const _ , _ -> st (* nothing to do *)
-        | CastE (t, e), c_typed ->
+        | CastE (k, t, e), c_typed ->
           begin match Cil.unrollType t, c_typed with
             | TFloat (_, _), Float c ->
               (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
@@ -864,7 +864,7 @@ struct
                       fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
                   | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
                | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
-            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (t, e))) st
+            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (k, t, e))) st
           end
         | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in

src/analyses/condVars.ml

@@ -18,7 +18,7 @@ module Domain = struct
   and var_in_expr p = function
     | Const _ | SizeOf _ | SizeOfStr _ | AlignOf _ -> true
     | Lval l | AddrOf l | StartOf l -> var_in_lval p l
-    | SizeOfE e | AlignOfE e | UnOp (_,e,_) | CastE (_,e) | Imag e | Real e -> var_in_expr p e
+    | SizeOfE e | AlignOfE e | UnOp (_,e,_) | CastE (_,_,e) | Imag e | Real e -> var_in_expr p e
     | BinOp (_,e1,e2,_) -> var_in_expr p e1 && var_in_expr p e2
     | Question (c,t,e,_) -> var_in_expr p c && var_in_expr p t && var_in_expr p e
     | AddrOfLabel _ -> true

src/analyses/malloc_null.ml

@@ -70,7 +70,7 @@ struct
 
   let get_concrete_exp (exp:exp) gl (st:D.t) =
     match constFold true exp with
-    | CastE (_,Lval (Var v, offs))
+    | CastE (_,_,Lval (Var v, offs))
     | Lval (Var v, offs) -> Some (Var v,offs)
     | _ -> None
 

src/analyses/memOutOfBounds.ml

@@ -46,7 +46,7 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> exp_contains_a_ptr e
+    | CastE (_, _, e) -> exp_contains_a_ptr e
     | BinOp (_, e1, e2, _) ->
       exp_contains_a_ptr e1 || exp_contains_a_ptr e2
     | Question (e1, e2, e3, _) ->
@@ -172,7 +172,7 @@ struct
       match ofs with
       | NoOffset -> `NoOffset
       | Field (fld, ofs) -> `Field (fld, convert_offset ofs)
-      | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
+      | Index (exp, ofs) when Offset.Index.Exp.is_any exp -> (* special offset added by convertToQueryLval *)
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match man.ask (Queries.EvalInt exp) with
@@ -372,7 +372,7 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e
+    | CastE (_, _, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e
     | BinOp (bop, e1, e2, t) ->
       check_exp_for_oob_access man ~is_implicitly_derefed e1;
       check_exp_for_oob_access man ~is_implicitly_derefed e2

src/analyses/tutorials/taint.ml

@@ -45,7 +45,7 @@ struct
     | Imag e
     | SizeOfE e
     | AlignOfE e
-    | CastE (_,e)
+    | CastE (_,_,e)
     | UnOp (_,e,_) -> is_exp_tainted state e
     | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> false
     | Question (b, t, f, _) -> is_exp_tainted state b || is_exp_tainted state t || is_exp_tainted state f