Trace loop heads #5381
Trace loop heads #5381
Conversation
|
Rebased to check the XSD validation step fails on CI (fix clang format errors) |
|
Validation step should now pass - source code docs will still fail |
|
A refactor I could put on top of this: thk123#4 (just pulls more "business logic" out of the json/xml specific files |
thk123
force-pushed
the
trace-loop-heads
branch
3 times, most recently
from
18cbd54 to
b05045c
Compare
thk123
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #5381 +/- ##
========================================
Coverage 68.19% 68.19%
========================================
Files 1175 1176 +1
Lines 97504 97517 +13
========================================
+ Hits 66490 66502 +12
- Misses 31014 31015 +1
Continue to review full report at Codecov.
|
| @@ -0,0 +1,32 @@ | |||
| /*******************************************************************\ | |||
|
|
|||
| Module: Goto Programs | |||
There was a problem hiding this comment.
Nit: Not goto programs module 🌴
There was a problem hiding this comment.
What module would you prefer? It is in folder goto-programs?
There was a problem hiding this comment.
I think normally this just names the feature in the file, here it would be Structured Trace Utilities or something.
There was a problem hiding this comment.
This seems... pointless 😛 I've checked the coding standards and it says it should just mention author, so I'll delete this line
| @@ -0,0 +1,37 @@ | |||
| /*******************************************************************\ | |||
|
|
|||
| Module: Goto Programs | |||
|
|
||
| /// There are two kinds of step for location markers - location-only and | ||
| /// loop-head (for locations associated with the first step of a loop). | ||
| enum class default_step_kindt |
There was a problem hiding this comment.
Nomenclature taken from the docs which call these default steps 🤷
src/goto-programs/xml_goto_trace.cpp
Outdated
| @@ -18,10 +18,12 @@ Author: Daniel Kroening | |||
| #include <util/symbol.h> | |||
| #include <util/xml_irep.h> | |||
|
|
|||
| #include <algorithm> | |||
| Ensure even with sliced formulas, we get a location only step for | ||
| each iteration of the loop (called loop-heads) when using partial loops. | ||
|
|
||
| This test is checking the following json:(deleting the new lines after each \n to obtain |
|
|
||
| #include "structured_trace_util.h" | ||
| #include <algorithm> | ||
| default_step_kindt |
There was a problem hiding this comment.
⛏️ some new lines would be appreciated.
|
One travis job is timing out running the tests, hopefully unlucky - will try again. |
In the trace, we only output the first location of a sequence of same locations. However, we don't want to suppress loop head locations because they might come from different loop iterations. If we suppressed them it would be impossible to know in which loop iteration we are in.
Even though the slicing removes all the assignments, the loop heads are maintained in the test
Extend the documentation to cover the new version of location-only called loop-head.
Previously the JSON and XML trace printing was duplicating the logic for determing whether a trace step is a loop head
Consolidate the documentation - deleting the duplicated doxygen that was attached to the implementation as well as the declaration
Integrating @peterschrammel work for adding loop-heads to the trace. Loop-heads replace location-only trace steps for the specific instruction that is the start of the loop (i.e. has a back edge pointing to it). These are never removed from the trace, even when two loop-heads are adjacent to each other in the trace, allowing seeing how many times the trace goes through the loop. See the documentation changes for more details.