diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index e8be4de532..f0b2a45701 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -619,7 +619,7 @@ struct |> List.enum |> Enum.filter_map (fun (lincons1: Apron.Lincons1.t) -> (* filter one-vars and exact *) - (* TODO: exact filtering doesn't really work with octagon because it returns two SUPEQ constraints instead *) + (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *) if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then RD.cil_exp_of_lincons1 lincons1 |> Option.map e_inv diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 02459906d2..694dcad89d 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -730,7 +730,7 @@ struct |> List.enum |> Enum.filter_map (fun (lincons1: Apron.Lincons1.t) -> (* filter one-vars and exact *) - (* TODO: exact filtering doesn't really work with octagon because it returns two SUPEQ constraints instead *) + (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *) if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then RD.cil_exp_of_lincons1 lincons1 |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp)) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 04d4a2eaa9..2f1375c2ce 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -552,7 +552,9 @@ struct |> Enum.map (fun (lincons0: Lincons0.t) -> Lincons1.{lincons0; env = array_env} ) - |> List.of_enum + |> Lincons1Set.of_enum + |> (if Oct.manager_is_oct Man.mgr then Lincons1Set.simplify else Fun.id) + |> Lincons1Set.elements end (** With heterogeneous environments. *) @@ -808,6 +810,7 @@ sig module V: RV module Tracked: RelationDomain.Tracked + module Man: Manager val assert_inv : Queries.ask -> t -> exp -> bool -> bool Lazy.t -> t val eval_int : Queries.ask -> t -> exp -> bool Lazy.t -> Queries.ID.t @@ -928,6 +931,7 @@ struct let lcb = D.to_lincons_array (D.of_lincons_array (BoxD.to_lincons_array b)) in (* convert through D to make lincons use the same format *) let lcd = D.to_lincons_array d in Lincons1Set.(diff (of_earray lcd) (of_earray lcb)) + |> (if Oct.manager_is_oct D.Man.mgr then Lincons1Set.simplify else Fun.id) |> Lincons1Set.elements end diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml index 327e43e321..6a995e69de 100644 --- a/src/cdomains/apron/gobApron.apron.ml +++ b/src/cdomains/apron/gobApron.apron.ml @@ -38,6 +38,30 @@ struct let equal x y = Var.compare x y = 0 end +module Linexpr0 = +struct + include Linexpr0 + + (** Negate linear expression. *) + let neg (linexpr0: t): t = + let r = copy linexpr0 in + let n = Linexpr0.get_size r in + for i = 0 to n - 1 do + Linexpr0.set_coeff r i (Coeff.neg (Linexpr0.get_coeff r i)) + done; + Linexpr0.set_cst r (Coeff.neg (Linexpr0.get_cst r)); + r +end + +module Linexpr1 = +struct + include Linexpr1 + + (** Negate linear expression. *) + let neg (linexpr1: t): t = + {linexpr0 = Linexpr0.neg linexpr1.linexpr0; env = linexpr1.env} +end + module Lincons1 = struct include Lincons1 @@ -62,6 +86,12 @@ struct incr size ) x; !size + + (** Flip comparison operator in linear constraint, i.e., swap sides. *) + let flip (lincons1: t): t = + (* Apron constraints have rhs 0 and inequality only in one direction, so do the following: *) + (* e >= 0 -> e <= 0 -> -e >= 0 *) + make (Linexpr1.neg (get_linexpr1 lincons1)) (get_typ lincons1) end module Lincons1Set = @@ -74,6 +104,26 @@ struct Lincons1.{lincons0; env = array_env} ) |> of_enum + + (** Simplify (octagon) constraint set to replace two {!SUPEQ}-s with single {!EQ}. *) + let simplify (lincons1s: t): t = + fold (fun lincons1 acc -> + match Lincons1.get_typ lincons1 with + | SUPEQ -> + let flipped = Lincons1.flip lincons1 in + if mem flipped lincons1s then ( + if Lincons1.compare lincons1 flipped < 0 then ( + Lincons1.set_typ flipped EQ; (* reuse flipped copy for equality *) + add flipped acc + ) + else + acc + ) + else + add lincons1 acc + | _ -> + add lincons1 acc + ) lincons1s empty end module Texpr1 = diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index eee8bc8d01..fcab8f4b99 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -268,44 +268,55 @@ module CilOfApron (V: SV) = struct exception Unsupported_Linexpr1 + let longlong = TInt(ILongLong,[]) + + + (** 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 + (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1) + | None -> raise Unsupported_Linexpr1) + | _ -> raise Unsupported_Linexpr1 + + (** Returned boolean indicates whether returned expression should be negated. *) + let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v = + 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 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 + | _ -> + M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v; + raise Unsupported_Linexpr1 + + (** Returned booleans indicates whether returned expressions should be negated. *) let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) = - let longlong = TInt(ILongLong,[]) in - let coeff_to_const consider_flip (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 not consider_flip || Z.compare i Z.zero >= 0 then - Const (CInt(i,ILongLong,None)), false - else - (* attempt to negate if that does not cause an overflow *) - let cneg, truncation = truncateCilint ILongLong (Z.neg i) in - if truncation = NoTruncation then - Const (CInt((Z.neg i),ILongLong,None)), true - else - Const (CInt(i,ILongLong,None)), false - 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 - in - let expr = ref (fst @@ coeff_to_const false (Linexpr1.get_cst linexpr1)) in + let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in let append_summand (c:Coeff.union_5) v = - 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 coeff, flip = coeff_to_const true c in - let prod = BinOp(Mult, coeff, var, longlong) in - if flip then - expr := BinOp(MinusA,!expr,prod,longlong) - else - expr := BinOp(PlusA,!expr,prod,longlong) - | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1 - | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v; raise Unsupported_Linexpr1 + if not (Coeff.is_zero c) then + terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms in Linexpr1.iter append_summand linexpr1; - !expr + !terms let lcm_den linexpr1 = @@ -339,13 +350,27 @@ struct try let linexpr1 = Lincons1.get_linexpr1 lincons1 in let common_denominator = lcm_den linexpr1 in - let cilexp = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in - match Lincons1.get_typ lincons1 with - | EQ -> Some (Cil.constFold false @@ BinOp(Eq, cilexp, zero, TInt(IInt,[]))) - | SUPEQ -> Some (Cil.constFold false @@ BinOp(Ge, cilexp, zero, TInt(IInt,[]))) - | SUP -> Some (Cil.constFold false @@ BinOp(Gt, cilexp, zero, TInt(IInt,[]))) - | DISEQ -> Some (Cil.constFold false @@ BinOp(Ne, cilexp, zero, TInt(IInt,[]))) - | EQMOD _ -> None + let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in + let (nterms, pterms) = Tuple2.mapn (List.map snd) (List.partition fst terms) in (* partition terms into negative (nterms) and positive (pterms) *) + let fold_terms terms = + List.fold_left (fun acc term -> + match acc with + | None -> Some term + | Some exp -> Some (BinOp (PlusA, exp, term, longlong)) + ) None terms + |> Option.default zero + in + let lhs = fold_terms pterms in + let rhs = fold_terms nterms in (* negative terms are moved from Apron's lhs to our rhs, so they all become positive there *) + let binop = + match Lincons1.get_typ lincons1 with + | EQ -> Eq + | SUPEQ -> Ge + | SUP -> Gt + | DISEQ -> Ne + | EQMOD _ -> raise Unsupported_Linexpr1 + in + Some (Cil.constFold false @@ BinOp(binop, lhs, rhs, TInt(IInt,[]))) (* constFold removes multiplication by factor 1 *) with Unsupported_Linexpr1 -> None end diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t index 0d6ac5430f..7955499643 100644 --- a/tests/regression/36-apron/12-traces-min-rpb1.t +++ b/tests/regression/36-apron/12-traces-min-rpb1.t @@ -31,7 +31,7 @@ column: 3 function: main location_invariant: - string: (0LL - (long long )g) + (long long )h == 0LL + string: (long long )h == (long long )g type: assertion format: C - entry_type: location_invariant @@ -41,7 +41,7 @@ column: 3 function: t_fun location_invariant: - string: (0LL - (long long )g) + (long long )h == 0LL + string: (long long )h == (long long )g type: assertion format: C - entry_type: location_invariant @@ -51,7 +51,7 @@ column: 3 function: t_fun location_invariant: - string: (0LL - (long long )g) + (long long )h == 0LL + string: (long long )h == (long long )g type: assertion format: C @@ -163,7 +163,6 @@ format: c_expression - entry_type: flow_insensitive_invariant flow_insensitive_invariant: - string: '! multithreaded || (A_locked || ((0LL - (long long )g) + (long long )h - >= 0LL && (long long )g - (long long )h >= 0LL))' + string: '! multithreaded || (A_locked || (long long )g == (long long )h)' type: assertion format: C diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t index fd435cab3e..9814227a61 100644 --- a/tests/regression/36-apron/52-queuesize.t +++ b/tests/regression/36-apron/52-queuesize.t @@ -55,7 +55,7 @@ Without diff-box: column: 3 function: push location_invariant: - string: 2147483647LL - (long long )capacity >= 0LL + string: 2147483647LL >= (long long )capacity type: assertion format: C - entry_type: location_invariant @@ -65,7 +65,7 @@ Without diff-box: column: 3 function: push location_invariant: - string: (long long )free >= 0LL + string: (long long )used + (long long )free == (long long )capacity type: assertion format: C - entry_type: location_invariant @@ -75,7 +75,7 @@ Without diff-box: column: 3 function: push location_invariant: - string: (long long )capacity - (long long )free >= 0LL + string: (long long )free >= 0LL type: assertion format: C - entry_type: location_invariant @@ -85,8 +85,7 @@ Without diff-box: column: 3 function: push location_invariant: - string: ((0LL - (long long )capacity) + (long long )free) + (long long )used == - 0LL + string: (long long )capacity >= (long long )free type: assertion format: C - entry_type: location_invariant @@ -96,7 +95,7 @@ Without diff-box: column: 3 function: pop location_invariant: - string: 2147483647LL - (long long )capacity >= 0LL + string: 2147483647LL >= (long long )capacity type: assertion format: C - entry_type: location_invariant @@ -106,7 +105,7 @@ Without diff-box: column: 3 function: pop location_invariant: - string: (long long )free >= 0LL + string: (long long )used + (long long )free == (long long )capacity type: assertion format: C - entry_type: location_invariant @@ -116,7 +115,7 @@ Without diff-box: column: 3 function: pop location_invariant: - string: (long long )capacity - (long long )free >= 0LL + string: (long long )free >= 0LL type: assertion format: C - entry_type: location_invariant @@ -126,8 +125,7 @@ Without diff-box: column: 3 function: pop location_invariant: - string: ((0LL - (long long )capacity) + (long long )free) + (long long )used == - 0LL + string: (long long )capacity >= (long long )free type: assertion format: C @@ -186,7 +184,7 @@ With diff-box: column: 3 function: push location_invariant: - string: (long long )free >= 0LL + string: (long long )used + (long long )free == (long long )capacity type: assertion format: C - entry_type: location_invariant @@ -196,7 +194,7 @@ With diff-box: column: 3 function: push location_invariant: - string: (long long )capacity - (long long )free >= 0LL + string: (long long )free >= 0LL type: assertion format: C - entry_type: location_invariant @@ -206,8 +204,7 @@ With diff-box: column: 3 function: push location_invariant: - string: ((0LL - (long long )capacity) + (long long )free) + (long long )used == - 0LL + string: (long long )capacity >= (long long )free type: assertion format: C - entry_type: location_invariant @@ -217,7 +214,7 @@ With diff-box: column: 3 function: pop location_invariant: - string: (long long )free >= 0LL + string: (long long )used + (long long )free == (long long )capacity type: assertion format: C - entry_type: location_invariant @@ -227,7 +224,7 @@ With diff-box: column: 3 function: pop location_invariant: - string: (long long )capacity - (long long )free >= 0LL + string: (long long )free >= 0LL type: assertion format: C - entry_type: location_invariant @@ -237,8 +234,7 @@ With diff-box: column: 3 function: pop location_invariant: - string: ((0LL - (long long )capacity) + (long long )free) + (long long )used == - 0LL + string: (long long )capacity >= (long long )free type: assertion format: C @@ -253,7 +249,7 @@ Compare witnesses: column: 3 function: push location_invariant: - string: 2147483647LL - (long long )capacity >= 0LL + string: 2147483647LL >= (long long )capacity type: assertion format: C - entry_type: location_invariant @@ -263,7 +259,7 @@ Compare witnesses: column: 3 function: pop location_invariant: - string: 2147483647LL - (long long )capacity >= 0LL + string: 2147483647LL >= (long long )capacity type: assertion format: C --- diff --git a/tests/regression/46-apron2/98-issue-1511b.t b/tests/regression/46-apron2/98-issue-1511b.t index f7c460b428..ad85405bf2 100644 --- a/tests/regression/46-apron2/98-issue-1511b.t +++ b/tests/regression/46-apron2/98-issue-1511b.t @@ -15,29 +15,29 @@ unsupported: 0 disabled: 0 total validation entries: 26 - [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: ((long long )j + (long long )d) + 2147483648LL >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: ((long long )k + (long long )d) + 2147483647LL >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: ((long long )k + (long long )j) + 2147483646LL >= 0LL (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (long long )d + 2147483648LL >= (long long )j (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (long long )d + 2147483649LL >= (long long )k (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (long long )j + 1LL >= (long long )k (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (long long )j + 2147483647LL >= (long long )d (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )d (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )j (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: 1LL >= (long long )k + (long long )j (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: 2147483647LL >= (long long )j + (long long )d (98-issue-1511b.c:22:5) + [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + (long long )d (98-issue-1511b.c:22:5) [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:22:5) - [Success][Witness] invariant confirmed: (1LL + (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (1LL - (long long )j) - (long long )k >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483646LL + (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483646LL - (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483646LL - (long long )j) + (long long )k >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483647LL + (long long )d) + (long long )k >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483647LL - (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) + (long long )j >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483648LL + (long long )d) - (long long )j >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483648LL - (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:27:5) - [Success][Witness] invariant confirmed: (2147483649LL + (long long )d) - (long long )k >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: ((long long )j + (long long )d) + 2147483648LL >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: ((long long )k + (long long )d) + 2147483647LL >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: ((long long )k + (long long )j) + 2147483646LL >= 0LL (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (long long )d + 2147483648LL >= (long long )j (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (long long )d + 2147483649LL >= (long long )k (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (long long )j + 1LL >= (long long )k (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (long long )j + 2147483647LL >= (long long )d (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )d (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )j (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: 1LL >= (long long )k + (long long )j (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: 2147483647LL >= (long long )j + (long long )d (98-issue-1511b.c:27:5) + [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + (long long )d (98-issue-1511b.c:27:5) [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:27:5)