Skip to content

Improving parameter of math function abs in condition#1253

Merged
michael-schwarz merged 7 commits intomasterfrom
no-overflow-sqrt
Nov 21, 2023
Merged

Improving parameter of math function abs in condition#1253
michael-schwarz merged 7 commits intomasterfrom
no-overflow-sqrt

Conversation

@stilscher
Copy link
Copy Markdown
Member

@stilscher stilscher commented Nov 17, 2023

PR for issue #1244

@stilscher
Copy link
Copy Markdown
Member Author

stilscher commented Nov 17, 2023

The value of the parameter of abs (in the example from the issue data) is not improved correctly yet. The problem seems to be, that the case that was implemented in the last commit is never reached. Before it jumps to the fallback implementation of invariant when trying to cast a float to a long because this case is not handled specifically.

analyzer/src/analyses/baseInvariant.ml

Lines 771 to 785 in 933b4e3

| CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
(match eval e st with
| Int i ->
if ID.leq i (ID.cast_to ik i) then
match unrollType (Cilfacade.typeOf e) with
| TInt(ik_e, _)
| TEnum ({ekind = ik_e; _ }, _) ->
(* let c' = ID.cast_to ik_e c in *)
let c' = ID.cast_to ik_e (ID.meet c (ID.cast_to ik (ID.top_of ik_e))) in (* TODO: cast without overflow, is this right for normal invariant? *)
if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a\n" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
inv_exp (Int c') e st
| x -> fallback (GobPretty.sprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st
else
fallback (GobPretty.sprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
| v -> fallback (GobPretty.sprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)

@michael-schwarz michael-schwarz linked an issue Nov 18, 2023 that may be closed by this pull request
Low-Hanging Fruits in SV-COMP No-Overflow: CWE190-*-square*.i #1244
Closed
@michael-schwarz michael-schwarz mentioned this pull request Nov 18, 2023
Merged
@michael-schwarz michael-schwarz merged commit 66ebc90 into master Nov 21, 2023
@michael-schwarz michael-schwarz deleted the no-overflow-sqrt branch November 21, 2023 12:27
@sim642
Copy link
Copy Markdown
Member

sim642 commented Nov 21, 2023

I don't think this draft should've been merged. #1254 contained the immediate solution but making it less ad-hoc in BaseInvariant is still a separate matter to look at.

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Nov 21, 2023

Ah, sorry, I merged the wrong thing.

@sim642
Copy link
Copy Markdown
Member

sim642 commented Nov 21, 2023

Or maybe it automatically merged this because it was included in #1254. Because both got merged.

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Nov 21, 2023

Ah, yes, that is what happened. I'll open it again

@michael-schwarz michael-schwarz restored the no-overflow-sqrt branch November 21, 2023 13:01
@sim642 sim642 mentioned this pull request Nov 27, 2023
Merged
@FelixKrayer FelixKrayer mentioned this pull request Nov 29, 2023
Merged
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Low-Hanging Fruits in SV-COMP No-Overflow: CWE190-*-square*.i

3 participants

@stilscher @sim642 @michael-schwarz