Merge pull request #766 from goblint/apron-ikind

Follow-up crash fixes to Apron and invariants

Author: sim642

.semgrep/cil.yml

@@ -5,6 +5,7 @@ rules:
       - pattern: Cil.typeOfLval
       - pattern: Cil.typeOfInit
       - pattern: Cil.typeOffset
+      - pattern: Cil.mkCast
       - pattern: Cil.get_stmtLoc
     paths:
       exclude:

src/analyses/apron/apronAnalysis.apron.ml

@@ -144,15 +144,15 @@ struct
 
   let assert_type_bounds apr x =
     assert (AD.varinfo_tracked x);
-    let ik = Cilfacade.get_ikind x.vtype in
-    if not (IntDomain.should_ignore_overflow ik) then ( (* don't add type bounds for signed when assume_none *)
+    match Cilfacade.get_ikind x.vtype with
+    | ik when not (IntDomain.should_ignore_overflow ik) -> (* don't add type bounds for signed when assume_none *)
       let (type_min, type_max) = IntDomain.Size.range ik in
       (* TODO: don't go through CIL exp? *)
       let apr = AD.assert_inv apr (BinOp (Le, Lval (Cil.var x), (Cil.kintegerCilint ik (Cilint.cilint_of_big_int type_max)), intType)) false in
       let apr = AD.assert_inv apr (BinOp (Ge, Lval (Cil.var x), (Cil.kintegerCilint ik (Cilint.cilint_of_big_int type_min)), intType)) false in
       apr
-    )
-    else
+    | _
+    | exception Invalid_argument _ ->
       apr
 
 

src/analyses/base.ml

@@ -511,7 +511,7 @@ struct
       let toInt i =
         match IdxDom.to_int @@ ID.cast_to ik i with
         | Some x -> Const (CInt (x,ik, None))
-        | _ -> mkCast ~e:(Const (CStr ("unknown",No_encoding))) ~newt:intType
+        | _ -> Cilfacade.mkCast ~e:(Const (CStr ("unknown",No_encoding))) ~newt:intType
 
       in
       match o with

src/cdomains/apron/apronDomain.apron.ml

@@ -269,11 +269,12 @@ struct
             | BinOp (Mod, e1, e2, _) ->
               Binop (Mod, texpr1_expr_of_cil_exp e1, texpr1_expr_of_cil_exp e2, Int, Near)
             | CastE (TInt _ as t, e) ->
-              begin match Cilfacade.typeOf e with
-                | e_typ when IntDomain.Size.is_cast_injective ~from_type:e_typ ~to_type:t -> (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *)
+              begin match IntDomain.Size.is_cast_injective ~from_type:(Cilfacade.typeOf e) ~to_type:t with (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *)
+                | true ->
                   Unop (Cast, texpr1_expr_of_cil_exp e, Int, Zero) (* TODO: what does Apron Cast actually do? just for floating point and rounding? *)
-                | _
-                | exception Cilfacade.TypeOfError _ -> (* typeOf inner e, not outer exp *)
+                | false
+                | exception Cilfacade.TypeOfError _ (* typeOf inner e, not outer exp *)
+                | exception Invalid_argument _ -> (* get_ikind in is_cast_injective *)
                   raise Unsupported_CilExp
               end
             | _ ->
@@ -289,7 +290,8 @@ struct
               raise Unsupported_CilExp
           );
           expr
-        | exception Cilfacade.TypeOfError _ ->
+        | exception Cilfacade.TypeOfError _
+        | exception Invalid_argument _ ->
           raise Unsupported_CilExp
     in
     texpr1_expr_of_cil_exp
@@ -366,7 +368,7 @@ struct
       match V.to_cil_varinfo fundec v with
       | Some vinfo ->
         (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *)
-        let var = Cil.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+        let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
         let coeff, flip = coeff_to_const true c in
         let prod = BinOp(Mult, coeff, var, longlong) in
         if flip then
@@ -884,7 +886,8 @@ struct
   let eval_int d e =
     let module ID = Queries.ID in
     match Cilfacade.get_ikind_exp e with
-    | exception Cilfacade.TypeOfError _ ->
+    | exception Cilfacade.TypeOfError _
+    | exception Invalid_argument _ ->
       ID.top () (* real top, not a top of any ikind because we don't even know the ikind *)
     | ik ->
       if M.tracing then M.trace "apron" "eval_int: exp_is_cons %a = %B\n" d_plainexp e (exp_is_cons e);

src/cdomains/intDomain.ml

@@ -319,7 +319,7 @@ struct
   let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
   let to_yojson x = I.to_yojson x.v
   let invariant e x =
-    let e' = Cil.(mkCast ~e ~newt:(TInt (x.ikind, []))) in
+    let e' = Cilfacade.mkCast ~e ~newt:(TInt (x.ikind, [])) in
     I.invariant_ikind e' x.ikind x.v
   let tag x = I.tag x.v
   let arbitrary ik = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."

src/util/cilfacade.ml

@@ -315,16 +315,14 @@ let getFuns fileAST : startfuns =
 let getFirstStmt fd = List.hd fd.sbody.bstmts
 
 
-(* Returns the ikind of a TInt(_) and TEnum(_). Unrolls typedefs. Warns if a a different type is put in and return IInt *)
+(* Returns the ikind of a TInt(_) and TEnum(_). Unrolls typedefs. *)
 let rec get_ikind t =
   (* important to unroll the type here, otherwise problems with typedefs *)
   match Cil.unrollType t with
   | TInt (ik,_)
   | TEnum ({ekind = ik; _},_) -> ik
   | TPtr _ -> get_ikind !Cil.upointType
-  | _ ->
-    Messages.warn "Something that we expected to be an integer type has a different type, assuming it is an IInt";
-    Cil.IInt
+  | _ -> invalid_arg ("Cilfacade.get_ikind: non-integer type " ^ CilType.Typ.show t)
 
 let ptrdiff_ikind () = get_ikind !ptrdiffType
 
@@ -444,6 +442,16 @@ and typeOffset basetyp =
     | _ -> raise (TypeOfError Field_NonCompound)
 
 
+(** {!Cil.mkCast} using our {!typeOf}. *)
+let mkCast ~(e: exp) ~(newt: typ) =
+  let oldt =
+    try
+      typeOf e
+    with TypeOfError _ -> (* e might involve alloc variables, weird offsets, etc *)
+      Cil.voidType (* oldt is only used for avoiding duplicate cast, so this falls back to adding cast *)
+  in
+  Cil.mkCastT ~e ~oldt ~newt
+
 let get_ikind_exp e = get_ikind (typeOf e)