From 975c3e1017af92b8fcdb21aa555675e0a026cc4f Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 28 Feb 2025 09:43:35 +0100 Subject: [PATCH 1/5] more precise exceptions, tracing for conversion rate statistics --- src/cdomains/apron/sharedFunctions.apron.ml | 41 +++++++++++++-------- 1 file changed, 26 insertions(+), 15 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 464c10ec74..c2494a5f12 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -53,13 +53,14 @@ 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 ("Exp_not_supported: "^(CilType.Exp.show e))] (** Expression constructor not supported. *) | 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. *) + | Invalid_argument of string (** Invalid argument. *) + | Ask_yields_bot of exp[@printer fun ppf e -> Format.pp_print_string ppf ("Ask_yields_bot on "^(CilType.Exp.show e))] (** Expression on bot context. *) [@@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 +93,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 (Invalid_argument 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 +111,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 -> raise (Unsupported_CilExp (Ask_yields_bot e)) (* TODO: This happens when called on a pointer type; we should establish the type bounds instead *) | `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 +150,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 (Invalid_argument 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,13 +168,13 @@ struct Binop (Div, texpr1 e1, texpr1 e2, Int, Zero) | CastE (TInt (t_ik, _) as t, e) -> 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 (Invalid_argument a)) | true -> texpr1 e | false -> (* Cast is not injective - we now try to establish suitable ranges manually *) (* 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 (Invalid_argument a)) in (* convert response to a constant *) IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res in match const with @@ -189,21 +190,31 @@ struct | exception Invalid_argument _ -> raise (Unsupported_CilExp (Cast_not_injective t)) end - | _ -> - raise (Unsupported_CilExp Exp_not_supported) + | BinOp _ -> + raise (Unsupported_CilExp (BinOp_not_supported)) + | 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 (Invalid_argument 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 @@ -226,7 +237,7 @@ struct | Ne -> (texpr1_1, texpr1_2, DISEQ) (* e1 != e2 ==> e1 - e2 != 0 *) | _ -> raise (Unsupported_CilExp BinOp_not_supported) end - | _ -> raise (Unsupported_CilExp Exp_not_supported) + | _ -> raise (Unsupported_CilExp (Exp_not_supported e)) in let inverse_typ = function | EQ -> DISEQ From 4a47201f36e4af5f8b337e7fa315d8c4849fd3c1 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Mon, 3 Mar 2025 09:54:47 +0100 Subject: [PATCH 2/5] not raising for a bottom in query boosts convesion rate a lot --- src/cdomains/apron/sharedFunctions.apron.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index c2494a5f12..6d0f9513f9 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -111,7 +111,7 @@ struct let query e ik = let res = match ask.f (EvalInt e) with - | `Bot -> raise (Unsupported_CilExp (Ask_yields_bot e)) (* TODO: This happens when called on a pointer type; we should establish the type bounds instead *) + | `Bot (* This happens when called on a pointer type; -> we can safely return top based on the ikind *) | `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; From 03763401cc898cb868aa466e35d1a8b5434db960 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Tue, 4 Mar 2025 11:21:53 +0100 Subject: [PATCH 3/5] more detailed statistics --- src/cdomains/apron/sharedFunctions.apron.ml | 36 +++++++++++++++++---- 1 file changed, 30 insertions(+), 6 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 6d0f9513f9..89ff28767b 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -53,10 +53,34 @@ 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 of exp[@printer fun ppf e -> Format.pp_print_string ppf ("Exp_not_supported: "^(CilType.Exp.show e))] (** Expression constructor not supported. *) + | Exp_not_supported of exp[@printer fun ppf e -> + let expvar = match e with + | Lval (Var _, Field _) -> "LVal Var.FieldAccessor" + | Lval (Var _, Index _) -> "LVal Var.Index" + | Lval (Mem _, Field _) -> "LVal Mem.FieldAccessor" + | Lval (Mem _, Index _) -> "LVal Mem.Index" + | Lval (Mem _, NoOffset) -> "LVal Mem" + | Lval (Var v, NoOffset) ->"LVal Var(untracked): "^(CilType.Varinfo.show v) + | Const _ -> "Const" + | SizeOf _ | SizeOfE _ | SizeOfStr _ -> "SizeOfXxx" + | AlignOf _ | AlignOfE _ -> "AlignOfXxx" + | UnOp (op,_,_) -> "UnOp"^(match op with | Neg -> "Neg" | BNot -> "BNot" | LNot -> "LNot") + | BinOp _ -> "BinOp" + | CastE _ -> "CastE" + | Question _ -> "Question" + | AddrOf _ | AddrOfLabel _ -> "AddrOfxxx" + | StartOf _ -> "StartOf" + | _ -> "Other" in + Format.pp_print_string ppf ("Exp_not_supported:"^expvar)] (** Expression constructor not supported. *) | 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. *) | Invalid_argument of string (** Invalid argument. *) | Ask_yields_bot of exp[@printer fun ppf e -> Format.pp_print_string ppf ("Ask_yields_bot on "^(CilType.Exp.show e))] (** Expression on bot context. *) [@@deriving show { with_path = false }] @@ -111,7 +135,7 @@ struct let query e ik = let res = match ask.f (EvalInt e) with - | `Bot (* This happens when called on a pointer type; -> we can safely return top based on the ikind *) + | `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; @@ -190,8 +214,8 @@ struct | exception Invalid_argument _ -> raise (Unsupported_CilExp (Cast_not_injective t)) end - | BinOp _ -> - raise (Unsupported_CilExp (BinOp_not_supported)) + | BinOp (op, _,_,_) -> + raise (Unsupported_CilExp (BinOp_not_supported op)) | e -> raise (Unsupported_CilExp (Exp_not_supported e)) in @@ -235,7 +259,7 @@ 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 e)) in From d162dcfb0273862697685c19a4aee30dd8c52d56 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 5 Mar 2025 09:51:21 +0100 Subject: [PATCH 4/5] comments --- src/cdomains/apron/sharedFunctions.apron.ml | 21 +-------------------- 1 file changed, 1 insertion(+), 20 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 89ff28767b..de41e7390e 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -53,25 +53,7 @@ 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 of exp[@printer fun ppf e -> - let expvar = match e with - | Lval (Var _, Field _) -> "LVal Var.FieldAccessor" - | Lval (Var _, Index _) -> "LVal Var.Index" - | Lval (Mem _, Field _) -> "LVal Mem.FieldAccessor" - | Lval (Mem _, Index _) -> "LVal Mem.Index" - | Lval (Mem _, NoOffset) -> "LVal Mem" - | Lval (Var v, NoOffset) ->"LVal Var(untracked): "^(CilType.Varinfo.show v) - | Const _ -> "Const" - | SizeOf _ | SizeOfE _ | SizeOfStr _ -> "SizeOfXxx" - | AlignOf _ | AlignOfE _ -> "AlignOfXxx" - | UnOp (op,_,_) -> "UnOp"^(match op with | Neg -> "Neg" | BNot -> "BNot" | LNot -> "LNot") - | BinOp _ -> "BinOp" - | CastE _ -> "CastE" - | Question _ -> "Question" - | AddrOf _ | AddrOfLabel _ -> "AddrOfxxx" - | StartOf _ -> "StartOf" - | _ -> "Other" in - Format.pp_print_string ppf ("Exp_not_supported:"^expvar)] (** 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 of binop [@printer fun ppf op -> Format.pp_print_string ppf (match op with @@ -82,7 +64,6 @@ type unsupported_cilExp = | Lt | Gt | Le | Ge | Eq | Ne -> "Comparison binop" | _ -> "other binop")](** BinOp constructor not supported. *) | Invalid_argument of string (** Invalid argument. *) - | Ask_yields_bot of exp[@printer fun ppf e -> Format.pp_print_string ppf ("Ask_yields_bot on "^(CilType.Exp.show e))] (** Expression on bot context. *) [@@deriving show { with_path = false }] (** Interface for Bounds which calculates bounds for expressions and is used inside the - Convert module. *) From 722e1bc492d363a3f389963d42b68eed642ff26e Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Wed, 5 Mar 2025 12:39:29 +0100 Subject: [PATCH 5/5] ikind-exception more transparently packaged --- src/cdomains/apron/sharedFunctions.apron.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index de41e7390e..013dca3405 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -63,7 +63,7 @@ type unsupported_cilExp = | LAnd | LOr -> "Logical binop" | Lt | Gt | Le | Ge | Eq | Ne -> "Comparison binop" | _ -> "other binop")](** BinOp constructor not supported. *) - | Invalid_argument of string (** Invalid argument. *) + | 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. *) @@ -98,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 a -> raise (Unsupported_CilExp (Invalid_argument a)) (* 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 @@ -155,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 a -> raise (Unsupported_CilExp (Invalid_argument a)) 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; @@ -173,13 +173,13 @@ struct Binop (Div, texpr1 e1, texpr1 e2, Int, Zero) | CastE (TInt (t_ik, _) as t, e) -> 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 a -> raise (Unsupported_CilExp (Invalid_argument a)) + | 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 *) (* 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 a -> raise (Unsupported_CilExp (Invalid_argument a)) 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 @@ -205,7 +205,7 @@ struct | exception (Cilfacade.TypeOfError _ as e) -> raise (Unsupported_CilExp (Exp_typeOf e)) | exception (Invalid_argument a) -> - raise (Unsupported_CilExp (Invalid_argument a)) + raise (Unsupported_CilExp (Ikind_non_integer a)) in texpr1_expr_of_cil_exp exp in