Dependency bug in "inlining" benchmark.


"If you run: Dependency.exe _v2.bpl /taint:v1.bpl_changed_lines.txt /prune /coarseDiff

You will find that the argument of the procedure should_not_taint is not tainted by dependency, although it should be.

Don’t be confused by the name of the procedure, only by using DAC we should be able to infer that the procedure is not tainted."

file attachments


nimrodpar wrote Aug 21, 2015 at 1:14 PM

From what i could make of it, the issue lies in the way argv is aliased.

In the main procedure, accessing argv is done through

In the foo() and bar() procedures, argv is accessed through the $M.1 map ($M.1 := $M.1[$p1 := 97];) and you can see that indeed for these 2 procedures the $M.1 map is tainted at the exit.

In main() however, argv is accessed through $M.2 so when foo() finishes, the taint does not flow to should_not_taint(), simply because $M.2 is not tainted.

This issue stems from the translation from C to boogie. SMACK must treat each pointer type as a different map, so char* is $M.1 and char** is $M.2, so there's an inherent separation there which is not really sound...

If you use the same pointer types for all pointers, this should resolve the issue, but we need to think how to overcome this in a more robust way.