Skip to content

Scope-based SymbExLogger Take 2#562

Merged
ArquintL merged 3 commits into
masterfrom
symb-ex-logger
Jul 7, 2021
Merged

Scope-based SymbExLogger Take 2#562
ArquintL merged 3 commits into
masterfrom
symb-ex-logger

Conversation

@ArquintL

@ArquintL ArquintL commented Jul 6, 2021

Copy link
Copy Markdown
Member

Introduces the same changes as #475.
Apparently, the changes introduced by the other PR have been added to master in commit 85ecb64 but apparently undone by accident in the next commit 73f7fd1.

This PR is almost identical except:

  • writeLogFile seems to no longer exist in the Silver codebase and thus the SymbExLogger will only use ideModeAdvanced (instead of looking at both flags) to decide whether it should be enabled or not
  • file validation has been enabled for the file/path passed as logConfig
  • some expected outputs for SymbExLogger tests had to be adapted. Looking two years back, it proved to be relatively robust:
    • Silicon does not seem to perform a Join operation in some cases after branching anymore, thus the corresponding Join record had to be removed
    • Caused by the change above, the numbering of some Silicon internal variables changes in the log output (they are used as path conditions). However, this could be made more robust in the future by e.g. extracting $t from $t@6@01
    • Silicon seems to print fields slightly different. This shows up in the symbLogTest_linkedListMinimal: previously, a branch has been logged as Branch $t@8@01 != Null: and nowadays it is Branch First:($t@6@01) != Null:

@aterga: these are the changes performed as part of my Master's thesis. I cannot recall whether we still support the old logging format and/or whether/how clients would need to be adapted. Could you maybe give it a try?

@ArquintL ArquintL requested a review from mschwerhoff July 6, 2021 09:43
@ArquintL

ArquintL commented Jul 6, 2021

Copy link
Copy Markdown
Member Author

All Silicon tests pass locally

@mschwerhoff mschwerhoff left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, thank you.

@ArquintL ArquintL merged commit b5c1365 into master Jul 7, 2021
@mschwerhoff mschwerhoff deleted the symb-ex-logger branch July 17, 2021 13:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants