Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closing the gaps in Texpr generation #1700

Merged
merged 7 commits into from
Mar 7, 2025
+33 −17
Merged

Closing the gaps in Texpr generation #1700

Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
975c3e1
more precise exceptions, tracing for conversion rate statistics
DrMichaelPetter Feb 28, 2025
4a47201
not raising for a bottom in query boosts convesion rate a lot
DrMichaelPetter Mar 3, 2025
0376340
more detailed statistics
DrMichaelPetter Mar 4, 2025
d162dcf
comments
DrMichaelPetter Mar 5, 2025
722e1bc
ikind-exception more transparently packaged
DrMichaelPetter Mar 5, 2025
5b6074d
Merge branch 'master' into stats_on_texpr
DrMichaelPetter Mar 5, 2025
3231002
Merge branch 'master' into stats_on_texpr
DrMichaelPetter Mar 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 33 additions & 17 deletions src/cdomains/apron/sharedFunctions.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
Loading