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.

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

Autotune for ana.malloc.unique_address_count for NoOverflows in SV-Comp #1612

Merged
merged 12 commits into from
Nov 7, 2024
Merged
Prev Previous commit
Next Next commit
Detect mallocs in loops instead of detecting mallocs outside of loops
karoliineh committed Nov 5, 2024
commit 4e7bfaeb472c4e60c4d84bb8ab7258297672f810
14 changes: 9 additions & 5 deletions src/autoTune.ml
Original file line number Diff line number Diff line change
@@ -45,20 +45,22 @@ class functionVisitor(calling, calledBy, argLists, dynamicallyCalled) = object
end

exception Found
class findAllocsNotInLoops = object
class findAllocsInLoops = object
inherit nopCilVisitor

val mutable inloop = false

method! vstmt stmt =
match stmt.skind with
| Loop _ -> SkipChildren
| Loop _ -> inloop <- true; DoChildren
karoliineh marked this conversation as resolved.
Show resolved Hide resolved
| _ -> DoChildren

method! vinst = function
| Call (_, Lval (Var f, NoOffset), args,_,_) ->
let desc = LibraryFunctions.find f in
begin match desc.special args with
| Malloc _
| Alloca _ -> raise Found
| Alloca _ when inloop -> raise Found
| _ -> DoChildren
end
| _ -> DoChildren
@@ -263,8 +265,10 @@ let noOverflows (spec: Svcomp.Specification.t) =
(*We focus on integer analysis*)
set_bool "ana.int.def_exc" true;
begin
try ignore @@ visitCilFileSameGlobals (new findAllocsNotInLoops) (!Cilfacade.current_file)
with Found -> set_int "ana.malloc.unique_address_count" 1;
try
ignore @@ visitCilFileSameGlobals (new findAllocsInLoops) (!Cilfacade.current_file);
set_int "ana.malloc.unique_address_count" 1
with Found -> set_int "ana.malloc.unique_address_count" 0;
end
| _ -> ()