Merge pull request #199 from goblint/cast-kind

Add cast kinds

Author: sim642

src/check.ml

@@ -601,7 +601,8 @@ and checkExp (isconst: bool) (e: exp) : typ =
           | _ -> E.s (bug "StartOf on a non-array")
       end
 
-      | CastE (tres, e) -> begin
+      | CastE (_, tres, e) -> begin
+        (* TODO: check castkind w.r.t. tres? *)
           let et = checkExp isconst e in
           checkType tres CTExp;
           (* Not all types can be cast *)

src/cil.ml

@@ -535,7 +535,7 @@ and exp =
   | Question   of exp * exp * exp * typ
                                         (** (a ? b : c) operation. Includes
                                             the type of the result *)
-  | CastE      of typ * exp            (** Use {!mkCast} to make casts *)
+  | CastE      of castkind * typ * exp (** Use {!mkCast} to make casts *)
 
   | AddrOf     of lval                 (** Always use {!mkAddrOf} to
                                           construct one of these. Apply to an
@@ -615,8 +615,15 @@ and binop =
   | LAnd                                (** logical and *)
   | LOr                                 (** logical or *)
 
-
-
+and castkind =
+  | Explicit (** Explicit conversion. @see C11 6.3.1. *)
+  | IntegerPromotion (** Integer promotion. @see C11 6.3.1.1.2. *)
+  | DefaultArgumentPromotion (** Default argument promotion. @see C11 6.5.2.2.6. *)
+  | ArithmeticConversion (** Usual arithmetic conversion. @see C11 6.3.1.8. *)
+  | ConditionalConversion (** Conditional conversion (non-standard terminology). @see C11 6.5.15.5 and 6.5.15.6. *)
+  | PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *)
+  | Implicit (** Implicit conversion. @see C11 6.3.1, 6.5.2.2.7, 6.5.2.4.2, 6.5.16.1.2, 6.5.16.2.3, 6.7.9.11, 6.8.4.2.5 and 6.8.6.4.3. *)
+  | Internal (** CIL-internal conversion (non-standard). *)
 
 (** An lvalue denotes the contents of a range of memory addresses. This range
    is denoted as a host object along with an offset within the object. The
@@ -1729,7 +1736,7 @@ let mkForIncr ~(iter : varinfo) ~(first: exp) ~stopat:(past: exp) ~(incr: exp)
 
 
 let rec stripCasts (e: exp) =
-  match e with CastE(_, e') -> stripCasts e' | _ -> e
+  match e with CastE(_, _, e') -> stripCasts e' | _ -> e
 
 
 
@@ -1909,7 +1916,7 @@ let getParenthLevel (e: exp) =
                                         (* Unary *)
   | Real _ -> 30
   | Imag _ -> 30
-  | CastE(_,_) -> 30
+  | CastE(_,_,_) -> 30
   | AddrOf(_) -> 30
   | AddrOfLabel(_) -> 30
   | StartOf(_) -> 30
@@ -1991,7 +1998,7 @@ let rec typeOf (e: exp) : typ =
   | UnOp (_, _, t)
   | BinOp (_, _, _, t)
   | Question (_, _, _, t)
-  | CastE (t, _) -> t
+  | CastE (_, t, _) -> t
   | AddrOf (lv) -> TPtr(typeOfLval lv, [])
   | AddrOfLabel (lv) -> voidPtrType
   | StartOf (lv) -> begin
@@ -2215,7 +2222,7 @@ let rec getInteger (e:exp) : cilint option =
   | Const(CInt (n, ik, _)) -> Some (mkCilintIk ik n)
   | Const(CChr c) -> getInteger (Const (charConstToInt c))
   | Const(CEnum(v, _, _)) -> getInteger v
-  | CastE(t, e) -> begin
+  | CastE(_, t, e) -> begin
       (* Handle any truncation due to cast. We optimistically ignore
 	 loss-of-precision due to floating-point casts. *)
       let mkInt ik n = Some (fst (truncateCilint ik n)) in
@@ -2622,19 +2629,19 @@ and constFold (machdep: bool) (e: exp) : exp =
       | _ -> constFold machdep (AlignOf (typeOf e))
   end
 
-  | CastE(it,
-          AddrOf (Mem (CastE(TPtr(bt, _), z)), off))
+  | CastE (k, it,
+          AddrOf (Mem (CastE(_, TPtr(bt, _), z)), off))
     when machdep && isZero z -> begin
       try
         let start, width = bitsOffset bt off in
         if start mod 8 <> 0 then
           E.s (error "Using offset of bitfield");
-        constFold machdep (CastE(it, (kinteger !kindOfSizeOf (start / 8))))
+        constFold machdep (CastE(k, it, (kinteger !kindOfSizeOf (start / 8))))
       with SizeOfError _ -> e
   end
 
 
-  | CastE (t, e) -> begin
+  | CastE (k, t, e) -> begin
       match constFold machdep e, unrollType t with
         (* Might truncate silently *)
       | Const(CInt(i,k,_)), TInt(nk,a)
@@ -2643,7 +2650,7 @@ and constFold (machdep: bool) (e: exp) : exp =
           when (dropAttributes ["const"; "pconst"] a) = [] ->
           let i', _ = truncateCilint nk (mkCilintIk k i) in
           Const(CInt(i', nk, None))
-      | e', _ -> CastE (t, e')
+      | e', _ -> CastE (k, t, e')
   end
   | Lval lv -> Lval (constFoldLval machdep lv)
   | AddrOf lv -> AddrOf (constFoldLval machdep lv)
@@ -2765,7 +2772,7 @@ let isArrayType t =
     An integer constant expr with value 0, or such an expr cast to void *, is called a null pointer constant. *)
 let isNullPtrConstant e =
   let rec isNullPtrConstant = function
-    | CastE (TPtr (TVoid [], []), e) -> isNullPtrConstant e (* no qualifiers allowed on void or ptr *)
+    | CastE (_, TPtr (TVoid [], []), e) -> isNullPtrConstant e (* no qualifiers allowed on void or ptr *)
     | e -> isZero e
   in
   isNullPtrConstant (constFold true e)
@@ -2781,7 +2788,7 @@ let rec isConstant = function
   | Real e -> isConstant e
   | Imag e -> isConstant e
   | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> true
-  | CastE (_, e) -> isConstant e
+  | CastE (_, _, e) -> isConstant e
   | AddrOf (Var vi, off) | StartOf (Var vi, off)
         -> vi.vglob && isConstantOffset off
   | AddrOf (Mem e, off) | StartOf(Mem e, off)
@@ -2875,6 +2882,17 @@ let d_binop () b =
   | LAnd -> text "&&"
   | LOr -> text "||"
 
+let d_castkind () k =
+  match k with
+  | Explicit -> text "Explicit"
+  | IntegerPromotion -> text "IntegerPromotion"
+  | DefaultArgumentPromotion -> text "DefaultArgumentPromotion"
+  | ArithmeticConversion -> text "ArithmeticConversion"
+  | ConditionalConversion -> text "ConditionalConversion"
+  | PointerConversion -> text "PointerConversion"
+  | Implicit -> text "Implicit"
+  | Internal -> text "Internal"
+
 let invalidStmt = mkStmt (Instr [])
 
 (** Construct a hash with the builtins *)
@@ -3405,9 +3423,12 @@ class defaultCilPrinterClass : cilPrinter = object (self)
           ++ text " : "
           ++ (self#pExpPrec level () e3)
 
-    | CastE(t,e) ->
+    | CastE(k,t,e) ->
         text "("
-          ++ self#pType None () t
+          ++ self#pType None () t (* TODO: option to not print implicit casts? *)
+          (* ++ text "/*"
+          ++ d_castkind () k (* convenient for debugging castkinds *)
+          ++ text "*/" *)
           ++ text ")"
           ++ self#pExpPrec level () e
 
@@ -3698,7 +3719,7 @@ class defaultCilPrinterClass : cilPrinter = object (self)
         in
         let patchArgNotUseVLACast exp =
           match exp with
-          | CastE(t, e) -> CastE(patchTypeNotVLA t, e)
+          | CastE(k, t, e) -> CastE(k, patchTypeNotVLA t, e)
           | e -> e
         in
         self#pLineDirective l
@@ -4698,7 +4719,7 @@ class plainCilPrinterClass =
               ++ unalign)
         ++ text ")"
 
-  | CastE(t,e) -> dprintf "CastE(@[%a,@?%a@])" self#pOnlyType t self#pExp e
+  | CastE(k,t,e) -> dprintf "CastE(@[%a,@?%a,@?%a@])" d_castkind k self#pOnlyType t self#pExp e
 
   | UnOp(u,e1,_) ->
       dprintf "UnOp(@[%a,@?%a@])"
@@ -5242,9 +5263,9 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
   | Question (e1, e2, e3, t) ->
       let e1' = vExp e1 in let e2' = vExp e2 in let e3' = vExp e3 in let t' = vTyp t in
       if e1' != e1 || e2' != e2 || e3' != e3 || t' != t then Question(e1',e2',e3',t') else e
-  | CastE (t, e1) ->
+  | CastE (k, t, e1) ->
       let t' = vTyp t in let e1' = vExp e1 in
-      if t' != t || e1' != e1 then CastE(t', e1') else e
+      if t' != t || e1' != e1 then CastE(k, t', e1') else e
   | AddrOf lv ->
       let lv' = vLval lv in
       if lv' != lv then AddrOf lv' else e
@@ -6097,7 +6118,7 @@ let getCompField (cinfo:compinfo) (fieldName:string) : fieldinfo =
   (List.find (fun fi -> fi.fname = fieldName) cinfo.cfields)
 
 
-let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
+let mkCastT ~(kind: castkind) ~(e: exp) ~(oldt: typ) ~(newt: typ) =
   (* Do not remove old casts because they are conversions !!! *)
   if Util.equals (typeSig oldt) (typeSig newt) then begin
     e
@@ -6109,11 +6130,11 @@ let mkCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
         let v = if compare i zero_cilint = 0 then zero_cilint else one_cilint in
         Const (CInt(v, IBool,  None))
     | TInt(newik, []), Const(CInt(i, _, _)) -> kintegerCilint newik i
-    | _ -> CastE(newt,e)
+    | _ -> CastE(kind,newt,e)
   end
 
-let mkCast ~(e: exp) ~(newt: typ) =
-  mkCastT ~e:e ~oldt:(typeOf e) ~newt:newt
+let mkCast ~kind ~(e: exp) ~(newt: typ) =
+  mkCastT ~kind ~e:e ~oldt:(typeOf e) ~newt:newt
 
 type existsAction =
     ExistsTrue                          (* We have found it *)
@@ -6230,7 +6251,7 @@ let rec makeZeroInit (t: typ) : init =
       CompoundInit (t', [])
 
   | TPtr _ as t ->
-      SingleInit(if !insertImplicitCasts then mkCast ~e:zero ~newt:t else zero)
+      SingleInit(if !insertImplicitCasts then mkCast ~kind:Internal ~e:zero ~newt:t else zero)
   | x -> E.s (unimp "Cannot initialize type: %a" d_type x)
 
 

src/cil.mli

@@ -617,7 +617,7 @@ and exp =
   | Question   of exp * exp * exp * typ
     (** (a ? b : c) operation. Includes the type of the result *)
 
-  | CastE      of typ * exp
+  | CastE      of castkind * typ * exp
     (** Use {!mkCast} to make casts.  *)
 
   | AddrOf     of lval
@@ -724,6 +724,16 @@ and binop =
                                            you want to use these, you must
                                            set {!useLogicalOperators}. *)
 
+and castkind =
+  | Explicit (** Explicit conversion. @see C11 6.3.1. *)
+  | IntegerPromotion (** Integer promotion. @see C11 6.3.1.1.2. *)
+  | DefaultArgumentPromotion (** Default argument promotion. @see C11 6.5.2.2.6. *)
+  | ArithmeticConversion (** Usual arithmetic conversion. @see C11 6.3.1.8. *)
+  | ConditionalConversion (** Conditional conversion (non-standard terminology). @see C11 6.5.15.5 and 6.5.15.6. *)
+  | PointerConversion (** Pointer conversion (non-standard). @see C11 6.5.6.8, 6.5.8.5 and 6.5.9.5. *)
+  | Implicit (** Implicit conversion. @see C11 6.3.1, 6.5.2.2.7, 6.5.2.4.2, 6.5.16.1.2, 6.5.16.2.3, 6.7.9.11, 6.8.4.2.5 and 6.8.6.4.3. *)
+  | Internal (** CIL-internal conversion (non-standard). *)
+
 (** {b Lvalues.} Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator.
 In C the syntax for lvalues is not always a good indication of the meaning
 of the lvalue. For example the C value
@@ -1717,10 +1727,10 @@ val mkString: string -> exp
 
 (** Construct a cast when having the old type of the expression. If the new
     type is the same as the old type, then no cast is added. *)
-val mkCastT: e:exp -> oldt:typ -> newt:typ -> exp
+val mkCastT: kind:castkind -> e:exp -> oldt:typ -> newt:typ -> exp
 
 (** Like {!mkCastT} but uses typeOf to get [oldt] *)
-val mkCast: e:exp -> newt:typ -> exp
+val mkCast: kind:castkind -> e:exp -> newt:typ -> exp
 
 (** Removes casts from this expression, but ignores casts within
   other expression constructs.  So we delete the (A) and (B) casts from
@@ -2386,6 +2396,9 @@ val d_binop: unit -> binop -> Pretty.doc
 (** Pretty-print a unary operator *)
 val d_unop: unit -> unop -> Pretty.doc
 
+(** Pretty-print a cast kind *)
+val d_castkind: unit -> castkind -> Pretty.doc
+
 (** Pretty-print an attribute using {!defaultCilPrinter}  *)
 val d_attr: unit -> attribute -> Pretty.doc
 

src/expcompare.ml

@@ -57,8 +57,8 @@ let rec compareExp (e1: exp) (e2: exp) : bool =
   | AddrOf lv1, AddrOf lv2 -> compareLval lv1 lv2
   | BinOp(bop1, l1, r1, _), BinOp(bop2, l2, r2, _) ->
       bop1 = bop2 && compareExp l1 l2 && compareExp r1 r2
-  | CastE(t1, e1), CastE(t2, e2) ->
-      t1 == t2 && compareExp e1 e2
+  | CastE(k1, t1, e1), CastE(k2, t2, e2) ->
+      k1 = k2 && t1 == t2 && compareExp e1 e2
   | _ -> begin
       match getInteger (constFold true e1), getInteger (constFold true e2) with
         Some i1, Some i2 -> compare_cilint i1 i2 = 0
@@ -95,7 +95,7 @@ and compareLval (lv1: lval) (lv2: lval) : bool =
    since they actually change the value of the expression. *)
 let rec stripNopCasts (e:exp): exp =
   match e with
-    CastE(t, e') -> begin
+    CastE(_, t, e') -> begin
       match unrollType (typeOf e'), unrollType t  with
         TPtr (bt1, a1), TPtr (bt2, a2)
           when isConstType bt1 = isConstType bt2 ->
@@ -127,7 +127,7 @@ let compareExpStripCasts (e1: exp) (e2: exp) : bool =
    of pointer arithmetic shouldn't change the resulting value. *)
 let rec stripCastsForPtrArith (e:exp): exp =
   match e with
-  | CastE(t, e') -> begin
+  | CastE(_, t, e') -> begin
       match unrollType (typeOf e'), unrollType t with
       (* Keep casts from void to something else.  Among other things,
          we keep casts from void* to char* that would otherwise be
@@ -209,7 +209,7 @@ let isTypeVolatile t =
 (* strip every cast between equal pointer types *)
 let rec stripCastsDeepForPtrArith (e:exp): exp =
   match e with
-  | CastE(t, e') when not(isTypeVolatile t) -> begin
+  | CastE(k, t, e') when not(isTypeVolatile t) -> begin
       let e' = stripCastsDeepForPtrArith e' in
       match unrollType (typeOf e'), unrollType t with
       (* Keep casts from void to something else.  Among other things,
@@ -224,11 +224,11 @@ let rec stripCastsDeepForPtrArith (e:exp): exp =
                isConstType bt1 = isConstType bt2 then
               e'
             else
-              CastE(t,e')
+              CastE(k,t,e')
           with SizeOfError _ -> (* bt1 or bt2 is abstract; don't strip. *)
-            CastE(t,e')
+            CastE(k,t,e')
         end
-      | _, _ -> CastE(t,e')
+      | _, _ -> CastE(k,t,e')
     end
   | UnOp(op,e,t) ->
       let e = stripCastsDeepForPtrArith e in
@@ -238,7 +238,7 @@ let rec stripCastsDeepForPtrArith (e:exp): exp =
       let e2 = stripCastsDeepForPtrArith e2 in
       if not(compareTypesNoAttributes ~ignoreSign:false
 	       (typeOf e1) (typeOf e2))
-      then BinOp(MinusPP, mkCast ~e:e1 ~newt:(typeOf e2), e2, t)
+      then BinOp(MinusPP, mkCast ~kind:PointerConversion ~e:e1 ~newt:(typeOf e2), e2, t)
       else BinOp(MinusPP, e1, e2, t)
   | BinOp(op,e1,e2,t) ->
       let e1 = stripCastsDeepForPtrArith e1 in

src/ext/dataslicing/dataslicing.ml

@@ -234,13 +234,13 @@ and sliceExp (i : int) (e : exp) : exp =
   | UnOp (op, e1, t) -> UnOp (op, sliceExp i e1, sliceType i t)
   | BinOp (op, e1, e2, t) -> BinOp (op, sliceExp i e1, sliceExp i e2,
                                     sliceType i t)
-  | CastE (t, e) -> sliceCast i t e
+  | CastE (k, t, e) -> sliceCast i k t e
   | AddrOf lv -> AddrOf (sliceLval i lv)
   | StartOf lv -> StartOf (sliceLval i lv)
   | SizeOf t -> SizeOf (sliceTypeAll t)
   | _ -> E.s (unimp "exp %a" d_exp e)
 
-and sliceCast (i : int) (t : typ) (e : exp) : exp =
+and sliceCast (i : int) (k : castkind) (t : typ) (e : exp) : exp =
   let te = typeOf e in
   match t, te with
   | TInt (k1, _), TInt (k2, attrs2) when k1 = k2 ->
@@ -250,9 +250,9 @@ and sliceCast (i : int) (t : typ) (e : exp) : exp =
       (* Note: We strip off integer cast operations. *)
       sliceExp i e
   | TPtr _, _ when isZero e ->
-      CastE (sliceType i t, sliceExp i e)
+      CastE (k, sliceType i t, sliceExp i e)
   | TPtr (bt1, _), TPtr (bt2, _) when (typeSig bt1) = (typeSig bt2) ->
-      CastE (sliceType i t, sliceExp i e)
+      CastE (k, sliceType i t, sliceExp i e)
   | _ ->
       E.s (unimp "sketchy cast (%a) -> (%a)\n" d_type te d_type t)
 

src/ext/pta/ptranal.ml

@@ -244,7 +244,7 @@ and analyze_expr (e : exp ) : A.tau =
       | UnOp (op, e, t) -> analyze_expr e
       | BinOp (op, e, e', t) -> A.join (analyze_expr e) (analyze_expr e')
       | Question (_, e, e', _) -> A.join (analyze_expr e) (analyze_expr e')
-      | CastE (t, e) -> analyze_expr e
+      | CastE (_, t, e) -> analyze_expr e
       | AddrOf l ->
           if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then
             A.rvalue (analyze_lval l)