-
Notifications
You must be signed in to change notification settings - Fork 43
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
XCFA-refactor 2023 [draft] #198
Conversation
@csanadtelbisz: Sonar fails, because some tests ultimately fail.
Can you take a look if this has something to do with the moved registerSolverFactories method in XcfaCli? I think I saw some modifications there in your pr (#202). Let me know if I'm mistaken. |
@leventeBajczi The solver issue arose due to the fact that |
A projection should be given in XcfaAnalysis.getXcfaAbstractor in order to avoid performance degradation compared to the original xcfa analysis, as the lack of non-trivial projection leads to a lot of unnecessary covering checks |
The WebDebuggerLogger is always enabled and it is responsible for a considerable portion of runtime. See the following lines: Lines 94 to 97 in c43d0a1
As it serves only debugging purposes, it should be disabled by default. @AdamZsofi git blame shows that you are the author of this change. The following profiler output confirms the problem. The WebDebuggerLogger takes ~1/3 (more than 10 seconds in this case) of all CPU time. |
Wrong result is given for the unreach-call property on the following tasks in the eca-rers2012 category of sv-benchmarks: Config 1: Config 2: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
All in all, this is an immense PR. I would like to ask for clarification on the following major things:
- With the (re)introduction of the LLVM frontend, Theta had its first cpp module. What is the relation between the
frontends/llvm
submodule, thelibtheta-llvm.so
library, and thetheta-c-frontend
repository?- If I interpret it correctly,
theta-c-frontend
was migrated intofrontends/llvm
, but without its project history, andlibtheta-llvm.so
is the built version offrontends/llvm
- Can we / should we migrate the history of
theta-c-frontend
? - Should we ship with a prebuilt version of
libtheta-llvm.so
?
- If I interpret it correctly,
- The XCFA
ProcedurePassManager
seems to enable no passes for CHC's. Is it intentional, or a regression error? - Other minor things in comments.
subprojects/frontends/llvm/src/main/cpp/passes/gazer/Intrinsics.cpp
Outdated
Show resolved
Hide resolved
subprojects/frontends/llvm/src/main/cpp/passes/gazer/Intrinsics.cpp
Outdated
Show resolved
Hide resolved
subprojects/frontends/llvm/src/main/cpp/passes/gazer/Intrinsics.h
Outdated
Show resolved
Hide resolved
subprojects/frontends/llvm/src/main/cpp/passes/gazer/Intrinsics.h
Outdated
Show resolved
Hide resolved
...nalysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt
Show resolved
Hide resolved
...mon/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/PartialSolver.kt
Show resolved
Hide resolved
subprojects/xcfa/cat/src/main/java/hu/bme/mit/theta/cat/solver/DatalogSolver.java
Outdated
Show resolved
Hide resolved
...smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java
Show resolved
Hide resolved
subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/ProcedurePassManager.kt
Outdated
Show resolved
Hide resolved
Thanks for the review! I'll get around to incorporating its findings hopefully this weekend. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@AdamZsofi WebDebuggerLogger still has an overhead, see the following lines:
Lines 94 to 95 in fdc40cf
String argGraph = JSONWriter.getInstance().writeString(ArgVisualizer.getDefault().visualize(arg)); | |
String precString = prec.toString(); |
This pull request adds support for pthread_mutex_init, pthread_cond_init, pthread_cond_wait, pthread_cond_signal as well as proper mutex support for static partial order reduction algorithms.
Changes have been implemented.
Quality Gate passedIssues Measures |
Benchexec test report for a selection of SV-Benchmarks (correct / incorrect / all): ✅ ConcurrencySafety-Main (3 / 0 / 5)
✅ ConcurrencySafety-MemSafety (4 / 0 / 5)
✅ ConcurrencySafety-NoOverflows (4 / 0 / 5)
✅ NoDataRace-Main (4 / 0 / 5)
❓ ReachSafety-Arrays (0 / 0 / 5)
✅ ReachSafety-BitVectors (2 / 0 / 5)
❓ ReachSafety-Combinations (0 / 0 / 5)
✅ ReachSafety-ControlFlow (1 / 0 / 5)
❓ ReachSafety-ECA (0 / 0 / 5)
✅ ReachSafety-Floats (3 / 0 / 5)
❓ ReachSafety-Hardware (0 / 0 / 5)
✅ ReachSafety-Heap (1 / 0 / 5)
❓ ReachSafety-Loops (0 / 0 / 5)
❓ ReachSafety-Recursive (0 / 0 / 5)
❓ ReachSafety-Sequentialized (0 / 0 / 5)
✅ ReachSafety-XCSP (1 / 0 / 5)
|
This PR merges the
xcfa-refactor
branch.Main features of the PR:
graph-solver
) to Thetalitmus-cli
for litmus test inputs