From 5f45f6a0dc88e38267e956165928ca2da870e80b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 10 Nov 2025 11:30:17 +0200 Subject: [PATCH 1/7] Avoid Cil.constFold in Apron invariant generation Instead of constant folding zero terms and one factors away, don't construct them in the first place. --- src/cdomains/apron/sharedFunctions.apron.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 446b9d792d..111ed66e4d 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -298,8 +298,11 @@ struct | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[])) -> let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in let flip, coeff = coeff_to_const ~scalewith c in - let prod = BinOp(Mult, coeff, var, longlong) in - flip, prod + if Z.equal (Option.get (Cil.getInteger coeff)) Z.one then (* Option.get should succeed by construction *) (* TODO: check (scaled!) coeff directly instead of extracting from exp *) + flip, var + else + let prod = BinOp(Mult, coeff, var, longlong) in + flip, prod | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1 @@ -309,7 +312,13 @@ struct (** Returned booleans indicates whether returned expressions should be negated. *) let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) = - let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in + let terms = + let c = Linexpr1.get_cst linexpr1 in + if Coeff.is_zero c then + ref [] + else + ref [coeff_to_const ~scalewith c] + in let append_summand (c:Coeff.union_5) v = if not (Coeff.is_zero c) then terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms @@ -369,7 +378,7 @@ struct | DISEQ -> Ne | EQMOD _ -> raise Unsupported_Linexpr1 in - Some (Cil.constFold false @@ BinOp(binop, lhs, rhs, TInt(IInt,[]))) (* constFold removes multiplication by factor 1 *) + Some (BinOp(binop, lhs, rhs, TInt(IInt,[]))) with Unsupported_Linexpr1 -> None end From 6b95d9617b1e33416d04ae70f0537cc44cb480f6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 8 Dec 2025 10:57:43 +0200 Subject: [PATCH 2/7] Fix "coefficient is not int" in wrong case in SharedFunctions --- src/cdomains/apron/sharedFunctions.apron.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 111ed66e4d..4b91b7dd9b 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -288,8 +288,10 @@ struct else false, Const (CInt(i,ILongLong,None)) else - (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1) - | None -> raise Unsupported_Linexpr1) + raise Unsupported_Linexpr1 + | None -> + M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; + raise Unsupported_Linexpr1) | _ -> raise Unsupported_Linexpr1 (** Returned boolean indicates whether returned expression should be negated. *) From 4df87a7d4bd3c53d67666c5c8d309be4c81acf49 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 8 Dec 2025 11:01:10 +0200 Subject: [PATCH 3/7] Extract SharedFunctions.int_of_coeff --- src/cdomains/apron/gobApron.apron.ml | 8 ++++ src/cdomains/apron/sharedFunctions.apron.ml | 43 +++++++++++---------- 2 files changed, 30 insertions(+), 21 deletions(-) diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml index 4511ca987a..fb16dcb82f 100644 --- a/src/cdomains/apron/gobApron.apron.ml +++ b/src/cdomains/apron/gobApron.apron.ml @@ -19,6 +19,14 @@ module Coeff = struct include Coeff + let pp = print + include Printable.SimpleFormat ( + struct + type nonrec t = t + let pp = pp + end + ) + let s_of_z z = Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z)) end diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 4b91b7dd9b..1059feb244 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -41,6 +41,10 @@ let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) = | _ -> failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar) +let int_of_coeff ?scalewith ?round (coeff: Coeff.union_5) = + match coeff with + | Scalar scalar -> int_of_scalar ?scalewith ?round scalar + | Interval _ -> None module type ConvertArg = sig @@ -272,27 +276,24 @@ struct (** Returned boolean indicates whether returned expression should be negated. *) let coeff_to_const ~scalewith (c:Coeff.union_5) = - match c with - | Scalar c -> - (match int_of_scalar ?scalewith c with - | Some i -> - let ci,truncation = truncateCilint ILongLong i in - if truncation = NoTruncation then - if Z.compare i Z.zero >= 0 then - false, Const (CInt(i,ILongLong,None)) - else - (* attempt to negate if that does not cause an overflow *) - let cneg, truncation = truncateCilint ILongLong (Z.neg i) in - if truncation = NoTruncation then - true, Const (CInt((Z.neg i),ILongLong,None)) - else - false, Const (CInt(i,ILongLong,None)) - else - raise Unsupported_Linexpr1 - | None -> - M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; - raise Unsupported_Linexpr1) - | _ -> raise Unsupported_Linexpr1 + match int_of_coeff ?scalewith c with + | Some i -> + let ci,truncation = truncateCilint ILongLong i in + if truncation = NoTruncation then + if Z.compare i Z.zero >= 0 then + false, Const (CInt(i,ILongLong,None)) + else + (* attempt to negate if that does not cause an overflow *) + let cneg, truncation = truncateCilint ILongLong (Z.neg i) in + if truncation = NoTruncation then + true, Const (CInt((Z.neg i),ILongLong,None)) + else + false, Const (CInt(i,ILongLong,None)) + else + raise Unsupported_Linexpr1 + | None -> + M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty c; + raise Unsupported_Linexpr1 (** Returned boolean indicates whether returned expression should be negated. *) let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v = From 00cceab072bce26a87c0592dd3f6a2563220451c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 8 Dec 2025 11:05:10 +0200 Subject: [PATCH 4/7] Extract SharedFunctions.CilOfApron.int_of_coeff_warn --- src/cdomains/apron/sharedFunctions.apron.ml | 34 +++++++++++---------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 1059feb244..5dc113896a 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -273,26 +273,28 @@ struct let longlong = TInt(ILongLong,[]) + let int_of_coeff_warn ?scalewith ?round coeff = + match int_of_coeff ?scalewith ?round coeff with + | Some i -> i + | None -> + M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty coeff; + raise Unsupported_Linexpr1 (** Returned boolean indicates whether returned expression should be negated. *) let coeff_to_const ~scalewith (c:Coeff.union_5) = - match int_of_coeff ?scalewith c with - | Some i -> - let ci,truncation = truncateCilint ILongLong i in - if truncation = NoTruncation then - if Z.compare i Z.zero >= 0 then - false, Const (CInt(i,ILongLong,None)) - else - (* attempt to negate if that does not cause an overflow *) - let cneg, truncation = truncateCilint ILongLong (Z.neg i) in - if truncation = NoTruncation then - true, Const (CInt((Z.neg i),ILongLong,None)) - else - false, Const (CInt(i,ILongLong,None)) + let i = int_of_coeff_warn ?scalewith c in + let ci,truncation = truncateCilint ILongLong i in + if truncation = NoTruncation then + if Z.compare i Z.zero >= 0 then + false, Const (CInt(i,ILongLong,None)) else - raise Unsupported_Linexpr1 - | None -> - M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty c; + (* attempt to negate if that does not cause an overflow *) + let cneg, truncation = truncateCilint ILongLong (Z.neg i) in + if truncation = NoTruncation then + true, Const (CInt((Z.neg i),ILongLong,None)) + else + false, Const (CInt(i,ILongLong,None)) + else raise Unsupported_Linexpr1 (** Returned boolean indicates whether returned expression should be negated. *) From 871a783a058cb630d99793aa540d8924cbc6cdf9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 8 Dec 2025 11:09:06 +0200 Subject: [PATCH 5/7] Make scalewith mandatory argument in SharedFunctions.CilOfApron --- src/cdomains/apron/sharedFunctions.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 5dc113896a..46080cfc0f 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -273,8 +273,8 @@ struct let longlong = TInt(ILongLong,[]) - let int_of_coeff_warn ?scalewith ?round coeff = - match int_of_coeff ?scalewith ?round coeff with + let int_of_coeff_warn ~scalewith coeff = + match int_of_coeff ~scalewith coeff with | Some i -> i | None -> M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty coeff; @@ -282,7 +282,7 @@ struct (** Returned boolean indicates whether returned expression should be negated. *) let coeff_to_const ~scalewith (c:Coeff.union_5) = - let i = int_of_coeff_warn ?scalewith c in + let i = int_of_coeff_warn ~scalewith c in let ci,truncation = truncateCilint ILongLong i in if truncation = NoTruncation then if Z.compare i Z.zero >= 0 then @@ -316,7 +316,7 @@ struct raise Unsupported_Linexpr1 (** Returned booleans indicates whether returned expressions should be negated. *) - let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) = + let cil_exp_of_linexpr1 ~scalewith (linexpr1:Linexpr1.t) = let terms = let c = Linexpr1.get_cst linexpr1 in if Coeff.is_zero c then From 1601a6fa2223c3350cca3f67b545c256d00d5b0f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 8 Dec 2025 11:11:34 +0200 Subject: [PATCH 6/7] Extract SharedFunctions.CilOfApron.cil_exp_of_int --- src/cdomains/apron/sharedFunctions.apron.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 46080cfc0f..5e68eeeded 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -281,8 +281,7 @@ struct raise Unsupported_Linexpr1 (** Returned boolean indicates whether returned expression should be negated. *) - let coeff_to_const ~scalewith (c:Coeff.union_5) = - let i = int_of_coeff_warn ~scalewith c in + let cil_exp_of_int i = let ci,truncation = truncateCilint ILongLong i in if truncation = NoTruncation then if Z.compare i Z.zero >= 0 then @@ -302,7 +301,8 @@ struct match V.to_cil_varinfo v with | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[])) -> let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in - let flip, coeff = coeff_to_const ~scalewith c in + let i = int_of_coeff_warn ~scalewith c in + let flip, coeff = cil_exp_of_int i in if Z.equal (Option.get (Cil.getInteger coeff)) Z.one then (* Option.get should succeed by construction *) (* TODO: check (scaled!) coeff directly instead of extracting from exp *) flip, var else @@ -322,7 +322,7 @@ struct if Coeff.is_zero c then ref [] else - ref [coeff_to_const ~scalewith c] + ref [cil_exp_of_int (int_of_coeff_warn ~scalewith c)] in let append_summand (c:Coeff.union_5) v = if not (Coeff.is_zero c) then From aeb2829f28a845e6bce98bb38d04c67b4315b621 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 8 Dec 2025 11:15:42 +0200 Subject: [PATCH 7/7] Remove roundabout conversion in SharedFunctions.CilOfApron.cil_exp_of_linexpr1_term --- src/cdomains/apron/sharedFunctions.apron.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 5e68eeeded..5ad1c5ab3e 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -302,12 +302,15 @@ struct | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[])) -> let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in let i = int_of_coeff_warn ~scalewith c in - let flip, coeff = cil_exp_of_int i in - if Z.equal (Option.get (Cil.getInteger coeff)) Z.one then (* Option.get should succeed by construction *) (* TODO: check (scaled!) coeff directly instead of extracting from exp *) - flip, var - else + if Z.equal i Z.one then + false, var + else if Z.equal i Z.minus_one then + true, var + else ( + let flip, coeff = cil_exp_of_int i in let prod = BinOp(Mult, coeff, var, longlong) in flip, prod + ) | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1