From 14d51d51fe952f6edad9871350f71cfccaea710d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Jul 2024 16:58:31 +0200 Subject: [PATCH 1/2] Check overflows when generating witnesses --- src/cdomains/apron/sharedFunctions.apron.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 4809e97917..a9406d48e9 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -274,7 +274,7 @@ struct let expr = ref (fst @@ coeff_to_const false (Linexpr1.get_cst linexpr1)) in let append_summand (c:Coeff.union_5) v = match V.to_cil_varinfo v with - | Some vinfo -> + | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[])) -> (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *) let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in let coeff, flip = coeff_to_const true c in @@ -284,6 +284,7 @@ struct else expr := BinOp(PlusA,!expr,prod,longlong) | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %s" (Var.to_string v); raise Unsupported_Linexpr1 + | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %s" (Var.to_string v); raise Unsupported_Linexpr1 in Linexpr1.iter append_summand linexpr1; !expr From 06ea5e050df7d03692912bbfc3022a068cf411f4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 17 Jul 2024 13:24:46 +0200 Subject: [PATCH 2/2] Rm resolved TODO --- src/cdomains/apron/sharedFunctions.apron.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index a9406d48e9..8121635e89 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -275,7 +275,6 @@ struct 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,[])) -> - (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *) 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 @@ -291,7 +290,7 @@ struct let lcm_den linexpr1 = - let exception UnsupportedScalar + let exception UnsupportedScalar in let frac_of_scalar scalar = if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)