Skip to content

Commit

Permalink
Merge pull request #1700 from goblint/stats_on_texpr
Browse files Browse the repository at this point in the history 
Closing the gaps in Texpr generation
  • Loading branch information
@DrMichaelPetter
DrMichaelPetter authored Mar 7, 2025
2 parents 50e8ab9 + 3231002 commit 66dff5a
Showing 1 changed file with 33 additions and 17 deletions.
50 changes: 33 additions & 17 deletions src/cdomains/apron/sharedFunctions.apron.ml
View file
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

0 comments on commit 66dff5a

Please sign in to comment.