search

goblint / bench

The benchmark suite
4 stars 5 forks source link

Import Ratcop benchmarks #33

Closed jerhard closed 1 year ago

jerhard commented 1 year ago

Import ratcop benchmarks from the analyzer repository.

jerhard commented 1 year ago

The way the number of unreachable asserts is computed in the benchmark script is only meaningful for fully inlined code; so the script should be changed to not report them. When looking at the results, these simply can be ignored for now.

jerhard commented 1 year ago

The way the number of unreachable asserts is computed in the benchmark script is only meaningful for fully inlined code; so the script should be changed to not report them. When looking at the results, these simply can be ignored for now.

The number of unreachable asserts is now no longer reported with the ratcop benchmark script.

jerhard commented 1 year ago

Would probably be a good idea to make that explicit in the conf.

What do mean exactly by that? To include threadJoins in the JSON conf? Would one then not explicitely have to deactivate it for all the configurations that don't need it?

sim642 commented 1 year ago

What do mean exactly by that? To include threadJoins in the JSON conf? Would one then not explicitely have to deactivate it for all the configurations that don't need it?

Yeah, I did that for the traces-rel-toy conf. Although the annoyance is that all the default analyses must also be copied into the conf, which is why I guess the traces-relational conf didn't have that. I don't think having threadJoins activated for all the others would change anything, because they don't use that information, which should be very cheap to compute as well. But as-is, it's fine to have it only for tid and cluster12 as arguments.

jerhard commented 1 year ago

traces-rel.json specifies to use --set sem.int.signed_overflow asssume_none; I restricted the use of this configuration of this to the two test cases where this option was used in the regression tests. E.g. for 17-mukherjee_sync01.c, one would not want to assume that no overflows happen.

sim642 commented 1 year ago

traces-rel.json specifies to use --set sem.int.signed_overflow asssume_none; I restricted the use of this configuration of this to the two test cases where this option was used in the regression tests. E.g. for 17-mukherjee_sync01.c, one would not want to assume that no overflows happen.

Reasonable enough, I think I changed it in the conf because otherwise operations after Apron widenings lead to many may-overflows, forgetting everything.