Skip to content

Commit

Permalink
Merge pull request #1258 from goblint/no_overflow_on_casts
Browse files Browse the repository at this point in the history
Do not set SV-COMP overflow flag on casts
  • Loading branch information
sim642 authored Nov 21, 2023
2 parents e8b880e + 464cdd3 commit 6b605c6
Show file tree
Hide file tree
Showing 4 changed files with 31 additions and 6 deletions.
12 changes: 6 additions & 6 deletions src/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3428,14 +3428,14 @@ module IntDomTupleImpl = struct
| Some(_, {underflow; overflow}) -> not (underflow || overflow)
| _ -> false

let check_ov ik intv intv_set =
let check_ov ~cast ik intv intv_set =
let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) in
if not no_ov && ( BatOption.is_some intv || BatOption.is_some intv_set) then (
let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in
let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in
let underflow = underflow_intv && underflow_intv_set in
let overflow = overflow_intv && overflow_intv_set in
set_overflow_flag ~cast:false ~underflow ~overflow ik;
set_overflow_flag ~cast ~underflow ~overflow ik;
);
no_ov

Expand All @@ -3444,7 +3444,7 @@ module IntDomTupleImpl = struct
let map x = Option.map fst x in
let intv = f p2 @@ r.fi2_ovc (module I2) in
let intv_set = f p5 @@ r.fi2_ovc (module I5) in
ignore (check_ov ik intv intv_set);
ignore (check_ov ~cast:false ik intv intv_set);
map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5)

let create2_ovc ik r x = (* use where values are introduced *)
Expand Down Expand Up @@ -3625,7 +3625,7 @@ module IntDomTupleImpl = struct
let map f ?no_ov = function Some x -> Some (f ?no_ov x) | _ -> None in
let intv = map (r.f1_ovc (module I2)) b in
let intv_set = map (r.f1_ovc (module I5)) e in
let no_ov = check_ov ik intv intv_set in
let no_ov = check_ov ~cast ik intv intv_set in
let no_ov = no_ov || should_ignore_overflow ik in
refine ik
( map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I1) x |> fst) a
Expand All @@ -3635,10 +3635,10 @@ module IntDomTupleImpl = struct
, BatOption.map fst intv_set )

(* map2 with overflow check *)
let map2ovc ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
let map2ovc ?(cast=false) ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
let intv = opt_map2 (r.f2_ovc (module I2)) xb yb in
let intv_set = opt_map2 (r.f2_ovc (module I5)) xe ye in
let no_ov = check_ov ik intv intv_set in
let no_ov = check_ov ~cast ik intv intv_set in
let no_ov = no_ov || should_ignore_overflow ik in
refine ik
( opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I1) x y |> fst) xa ya
Expand Down
7 changes: 7 additions & 0 deletions tests/regression/29-svcomp/32-no-ov.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
// PARAM: --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )"

int main(){
// This is not an overflow, just implementation defined behavior on a cast
int data = ((int)(rand() & 1 ? (((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) : -(((unsigned)rand()<<30) ^ ((unsigned)rand()<<15) ^ rand()) - 1));
return 0;
}
16 changes: 16 additions & 0 deletions tests/regression/29-svcomp/32-no-ov.t
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
$ goblint --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" 32-no-ov.c
SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (32-no-ov.c:5:6-5:159)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 3
dead: 0
total lines: 3
SV-COMP result: true
[Info][Race] Memory locations race summary:
safe: 1
vulnerable: 0
unsafe: 0
total memory locations: 1
2 changes: 2 additions & 0 deletions tests/regression/29-svcomp/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
(cram
(deps (glob_files *.c)))

0 comments on commit 6b605c6

Please sign in to comment.