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

make cil_exp_of_linexpr1 work with fractional expressions #1493

Merged
merged 11 commits into from
Jul 2, 2024
Merged

make cil_exp_of_linexpr1 work with fractional expressions #1493

Changes from 9 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
ab78123
[skip ci] int_of_scalar now returning Q.t
DrMichaelPetter May 28, 2024
bde040e
frac_of_scalar instead of int_of_scalar
DrMichaelPetter Jun 11, 2024
8920200
next try
DrMichaelPetter Jun 17, 2024
8eb76d0
Merge branch 'master' into issue_1328
DrMichaelPetter Jun 17, 2024
a7e4ff1
Update src/cdomains/apron/sharedFunctions.apron.ml
DrMichaelPetter Jun 18, 2024
7876d6b
Update src/cdomains/apron/sharedFunctions.apron.ml
DrMichaelPetter Jun 18, 2024
e4cd4df
Update src/cdomains/apron/sharedFunctions.apron.ml
DrMichaelPetter Jun 18, 2024
4fe33dc
make sure that exact division is possible
DrMichaelPetter Jun 28, 2024
4d5a408
removed unused parameter
DrMichaelPetter Jul 2, 2024
05dfb9f
pulled out product
DrMichaelPetter Jul 2, 2024
44e9549
Merge branch 'master' into issue_1328
DrMichaelPetter Jul 2, 2024
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
49 changes: 40 additions & 9 deletions src/cdomains/apron/sharedFunctions.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@ open GobApron

module M = Messages

let int_of_scalar ?round (scalar: Scalar.t) =

let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
None
else
Expand All @@ -20,18 +21,21 @@ let int_of_scalar ?round (scalar: Scalar.t) =
| None when Stdlib.Float.is_integer f -> Some f
| None -> None
in
Z.of_float f
Z.(of_float f * scalewith)
| Mpqf scalar -> (* octMPQ, boxMPQ, polkaMPQ *)
let n = Mpqf.get_num scalar in
let d = Mpqf.get_den scalar in
let scale = Z_mlgmpidl.mpz_of_z scalewith in
let+ z =
if Mpzf.cmp_int d 1 = 0 then (* exact integer (denominator 1) *)
Some n
Some (Mpzf.mul scale n)
else
begin match round with
| Some `Floor -> Some (Mpzf.fdiv_q n d) (* floor division *)
| Some `Ceil -> Some (Mpzf.cdiv_q n d) (* ceiling division *)
| None -> None
| Some `Floor -> Some (Mpzf.mul scale (Mpzf.fdiv_q n d)) (* floor division *)
| Some `Ceil -> Some (Mpzf.mul scale (Mpzf.cdiv_q n d)) (* ceiling division *)
| None -> if Mpz.divisible_p (Mpzf.mul scale n ) d then
Some (Mpzf.divexact (Mpzf.mul scale n ) d) (* scale, preferably with common denominator *)
else None
end
in
Z_mlgmpidl.z_of_mpzf z
Expand Down Expand Up @@ -245,11 +249,11 @@ module CilOfApron (V: SV) =
struct
exception Unsupported_Linexpr1

let cil_exp_of_linexpr1 (linexpr1:Linexpr1.t) =
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 c with
(match int_of_scalar ?scalewith c with
| Some i ->
let ci,truncation = truncateCilint ILongLong i in
if truncation = NoTruncation then
Expand Down Expand Up @@ -285,11 +289,38 @@ struct
!expr


let lcm_den linexpr1 =
let exception UnsupportedScalar
in
let frac_of_scalar scalar =
if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
None
else match scalar with
| Float f -> if Stdlib.Float.is_integer f then Some (Q.of_float f) else None
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

According to Zarith documentation, Q.of_float is exact, so shouldn't this also work for non-integers?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could, but in general, I would expect this case to happen, if we come from a float-based apron analysis. Correct me if I am wrong in the following argumentation:

These floats would likely stem from a floating point based analysis in apron, and thus would probably lead to very large denominators due to some +/-1 rounding in the low end of the mantissa. This might not hurt soundness so bad, since the result is only used to perform a scaling on the whole equality, but still the outcome might be very scary looking. In this implementation, I opted for a more conservative approach, just ignoring these floats.

| Mpqf f -> Some (Z_mlgmpidl.q_of_mpqf f)
| _ -> raise UnsupportedScalar
in
let extract_den (c:Coeff.union_5) =
match c with
| Scalar c -> BatOption.map Q.den (frac_of_scalar c)
| _ -> None
in
let lcm_denom = ref (BatOption.default Z.one (extract_den (Linexpr1.get_cst linexpr1))) in
let lcm_coeff (c:Coeff.union_5) _ =
match (extract_den c) with
| Some z -> lcm_denom := Z.lcm z !lcm_denom
| _ -> ()
in
try
Linexpr1.iter lcm_coeff linexpr1; !lcm_denom
with UnsupportedScalar -> Z.one

let cil_exp_of_lincons1 (lincons1:Lincons1.t) =
let zero = Cil.kinteger ILongLong 0 in
try
let linexpr1 = Lincons1.get_linexpr1 lincons1 in
let cilexp = cil_exp_of_linexpr1 linexpr1 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,[])))
Expand Down
Loading