-
Notifications
You must be signed in to change notification settings - Fork 58
Description
Looking at the random log from: https://sv-comp.sosy-lab.org/2024/results/results-verified/symbiotic.2023-11-28_20-34-48.results.SV-COMP24_unreach-call.ReachSafety-Loops.xml.bz2.fixed.xml.bz2.table.html#/table.
Current compilation flags are:
clang -c -emit-llvm -fgnu89-inline -D__inline= -Wno-unused-parameter -Wno-unknown-attributes -Wno-unused-label -Wno-unknown-pragmas -Wno-unused-command-line-argument -O0 -disable-O0-optnone -disable-llvm-passes -g -fbracket-depth=2048
After removing: -Wno-unused-command-line-argument the output is:
clang: warning: argument unused during compilation: '-disable-O0-optnone' [-Wunused-command-line-argument]
clang: warning: argument unused during compilation: '-disable-llvm-passes' [-Wunused-command-line-argument]
Mentioned flags come from: https://github.com/staticafi/symbiotic/blob/svcomp24/lib/symbioticpy/symbiotic/transform.py#L169
Problem:
Currently outputed LLVM IR file contains functions annotated with the optnone attribute, which suppresses essentially all optimizations on a function or method. In all later opt calls(?).
Solution
Replace mentioned flags with (I can prepare such a PR if you want):
-mllvm -disable-llvm-optzns -Xclang -disable-O0-optnone
But as I already tested it, for some reason, the sbt-slicer coredumps when these flags are used. I would need to do more investigation.
Some useful links: