Merge pull request #1700 from goblint/stats_on_texpr

Closing the gaps in Texpr generation

Author: DrMichaelPetter

src/cdomains/apron/sharedFunctions.apron.ml

@@ -53,13 +53,19 @@ module type SV =  RelationDomain.RV with type t = Var.t
 type unsupported_cilExp =
   | Var_not_found of CilType.Varinfo.t (** Variable not found in Apron environment. *)
   | Cast_not_injective of CilType.Typ.t (** Cast is not injective, i.e. may under-/overflow. *)
-  | Exp_not_supported (** Expression constructor not supported. *)
+  | Exp_not_supported of exp[@printer fun ppf e -> Format.pp_print_string ppf (GobPretty.show (Cil.d_plainexp () e))]
   | Overflow (** May overflow according to Apron bounds. *)
   | Exp_typeOf of exn [@printer fun ppf e -> Format.pp_print_string ppf (Printexc.to_string e)] (** Expression type could not be determined. *)
-  | BinOp_not_supported (** BinOp constructor not supported. *)
+  | BinOp_not_supported of binop [@printer fun ppf op -> Format.pp_print_string ppf (match op with
+        | BAnd | BOr | BXor -> "Bitwise binop"
+        | Shiftlt | Shiftrt -> "Shift binop"
+        | PlusPI | MinusPI | IndexPI | MinusPP -> "Pointer binop"
+        | LAnd | LOr -> "Logical binop"
+        | Lt | Gt | Le | Ge | Eq | Ne -> "Comparison binop"
+        | _ -> "other binop")](** BinOp constructor not supported. *)
+  | Ikind_non_integer of string (** Exception during trying to get ikind of a non-integer typed expression *)
 [@@deriving show { with_path = false }]
 
-
 (** Interface for Bounds which calculates bounds for expressions and is used inside the - Convert module. *)
 module type ConvBounds =
 sig
@@ -92,7 +98,7 @@ struct
       established by other analyses.*)
   let overflow_handling no_ov ik env expr d exp =
     match Cilfacade.get_ikind_exp exp with
-    | exception Invalid_argument e ->  raise (Unsupported_CilExp Exp_not_supported)       (* expression is not an integer expression, i.e. float *)
+    | exception Invalid_argument a ->  raise (Unsupported_CilExp (Ikind_non_integer a))       (* expression is not an integer expression, i.e. float *)
     | ik ->
       if IntDomain.should_wrap ik || not (Lazy.force no_ov) then (
         let (type_min, type_max) = IntDomain.Size.range ik in
@@ -110,7 +116,7 @@ struct
       let query e ik =
         let res =
           match ask.f (EvalInt e) with
-          | `Bot -> raise (Unsupported_CilExp Exp_not_supported) (* This should never happen according to Michael Schwarz *)
+          | `Bot  (* This happens when called on a pointer type; -> we can safely return top *)
           | `Top -> IntDomain.IntDomTuple.top_of ik
           | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in
         if M.tracing then M.trace "relation-query" "texpr1_expr_of_cil_exp/query: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty res;
@@ -149,7 +155,7 @@ struct
               *)
               let simplify e =
                 GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
-                let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)   in
+                let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))   in
                 let simp = query e ikind in
                 let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in
                 if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty simp;
@@ -167,14 +173,14 @@ struct
                 Binop (Div, texpr1 e1, texpr1 e2, Int, Zero)
               | CastE (t, e) when Cil.isIntegralType t ->
                 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? *)
-                  | exception Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)
+                  | exception Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))
                   | true -> texpr1 e
                   | false -> (* Cast is not injective - we now try to establish suitable ranges manually  *)
                     let t_ik = Cilfacade.get_ikind t in
                     (* retrieving a valuerange for a non-injective cast works by a query to the value-domain with subsequent value extraction from domtuple - which should be speculative, since it is not program code *)
                     let const,res = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
                       (* try to evaluate e by EvalInt Query *)
-                      let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported)  in
+                      let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))  in
                       (* convert response to a constant *)
                       IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res in
                     match const with
@@ -190,21 +196,31 @@ struct
                     | exception Invalid_argument _ ->
                       raise (Unsupported_CilExp (Cast_not_injective t))
                 end
-              | _ ->
-                raise (Unsupported_CilExp Exp_not_supported)
+              | BinOp (op, _,_,_) ->
+                raise (Unsupported_CilExp (BinOp_not_supported op))
+              | e ->
+                raise (Unsupported_CilExp (Exp_not_supported e))
             in
             overflow_handling no_ov ik env expr d exp;
             expr
-          | exception (Cilfacade.TypeOfError _ as e)
-          | exception (Invalid_argument _ as e) ->
+          | exception (Cilfacade.TypeOfError _ as e) ->
             raise (Unsupported_CilExp (Exp_typeOf e))
+          | exception (Invalid_argument a) ->
+            raise (Unsupported_CilExp (Ikind_non_integer a))
       in
       texpr1_expr_of_cil_exp exp
     in
     let exp = Cil.constFold false exp in
-    let res = conv exp in
-    if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
-    res
+    if M.tracing then 
+      match conv exp with
+      | exception Unsupported_CilExp ex -> 
+        M.tracel "rel-texpr-cil-conv" "unsuccessfull: %s" (show_unsupported_cilExp ex);
+        raise (Unsupported_CilExp ex)
+      | res -> 
+        M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
+        M.tracel "rel-texpr-cil-conv" "successfull: Good";
+        res
+    else conv exp
 
   let texpr1_of_cil_exp ask d env e no_ov =
     let res = texpr1_expr_of_cil_exp ask d env e no_ov in
@@ -225,9 +241,9 @@ struct
           | Ge -> (texpr1_1, texpr1_2, SUPEQ) (* e1 >= e2  ==>  e1 - e2 >= 0 *)
           | Eq -> (texpr1_1, texpr1_2, EQ)    (* e1 == e2  ==>  e1 - e2 == 0 *)
           | Ne -> (texpr1_1, texpr1_2, DISEQ) (* e1 != e2  ==>  e1 - e2 != 0 *)
-          | _ -> raise (Unsupported_CilExp BinOp_not_supported)
+          | _ -> raise (Unsupported_CilExp (BinOp_not_supported r))
         end
-      | _ -> raise (Unsupported_CilExp Exp_not_supported)
+      | _ -> raise (Unsupported_CilExp (Exp_not_supported e))
     in
     let inverse_typ = function
       | EQ -> DISEQ