Scope-based SymbExLogger by viper-admin · Pull Request #475 · viperproject/silicon

viper-admin · 2020-02-20T12:27:10Z

Pull request 🔀 created by @ArquintL on 2019-08-23 11:45
Last updated on 2020-02-14 14:40
Original Bitbucket pull request id: 65

Participants:

@mschwerhoff (reviewer)

@ArquintL

Source: 5670297 on branch arquintl/silicon/default
Destination: 76f21ec on branch master

State: OPEN

adds logConfig as additional Silicon config parameter
expects consolidateOnAssertTrue as additional SilFrontendConfig parameter (TODO LA: PR for silver)
adds implementation of new SymbExLogger with heavy code cleanup (it’s now more than 1 source file → viper.silicon.logger package
moves unit tests of SymbExLogger to a dedicated test file: SymbExLoggerTests
makes SymbExLogger unit tests more flexible by ignoring additional records and expecting only method, function, predicate, braching, joining, and execute records

…cords

…mbEx logger

…adds logger support for arbitrary CFG branching

… checker for exec time completeness on records

…unit tests

…nsolidation was performed next, and verification is retried

…cords as condition, pre-, or postcondition

…cs unit test is working

…nd scoping

…e not considered scopes, some runtime checks on logged paths, genericNode export

viper-admin · 2020-02-20T12:28:18Z

@ArquintL commented on 2019-10-01 15:16

Outdated location: line 17 of src/main/scala/logger/records/data/SingleMergeRecord.scala

Please change constant functions to actual constants, i.e. override val toTypeString: String = "single merge". This might require you to declare the abstract def toTypeString without parentheses.

Please do this for all such functions, I’ve noticed them in nearly all data records.

done

viper-admin · 2020-02-20T12:28:19Z

@ArquintL commented on 2019-10-01 15:24

Outdated location: line 1 of src/main/scala/logger/records/data/SingleMergeRecord.scala

MPL header missing.

Please check all files for missing MPL headers.

done

viper-admin · 2020-02-20T12:28:20Z

@ArquintL commented on 2019-10-01 15:24

Outdated location: line 1 of src/main/scala/logger/records/data/ProverAssertRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:21Z

@ArquintL commented on 2019-10-01 15:24

Outdated location: line 1 of src/main/scala/logger/records/data/ProduceRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:22Z

@ArquintL commented on 2019-10-01 15:24

Outdated location: line 1 of src/main/scala/logger/records/data/PredicateRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:23Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/MethodRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:24Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/MethodCallRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:25Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/MemberRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:26Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/ImpliesRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:27Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/FunctionRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:28Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/ExecuteRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:29Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/EvaluateRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:30Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/DeciderAssumeRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:31Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/DeciderAssertRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:31Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/DataRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:32Z

@ArquintL commented on 2019-10-01 15:25

Outdated location: line 1 of src/main/scala/logger/records/data/ConsumeRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:33Z

@ArquintL commented on 2019-10-01 15:26

Outdated location: line 1 of src/main/scala/logger/records/data/ConditionalEdgeRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:34Z

@ArquintL commented on 2019-10-01 15:26

Outdated location: line 1 of src/main/scala/logger/records/data/CondExpRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:35Z

@ArquintL commented on 2019-10-01 15:26

Outdated location: line 1 of src/main/scala/logger/records/data/CommentRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:36Z

@ArquintL commented on 2019-10-01 15:26

Outdated location: line 1 of src/main/scala/logger/records/SymbolicRecord.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:37Z

@ArquintL commented on 2019-10-01 15:26

Outdated location: line 1 of src/main/scala/logger/records/RecordData.scala

MPL header missing

done

viper-admin · 2020-02-20T12:28:38Z

@ArquintL commented on 2019-10-01 15:27

Outdated location: line 370 of src/main/scala/logger/SymbExLogger.scala

Appending to List has O(n) cost. Create Vectors instead of Lists or Seqs.

done

viper-admin · 2020-02-20T12:28:40Z

@ArquintL commented on 2019-10-01 15:27

Outdated location: line 1 of src/main/scala/logger/LogConfig.scala

MPL header is missing from file

done

viper-admin · 2020-02-20T12:28:41Z

@ArquintL commented on 2019-10-01 15:41

Outdated location: line 2 of src/test/resources/symbExLogTests/symbLogTest_ImpureBranching.sil.elog

Checking for these internal names seems to make the test case rather brittle. Are they really necessary?

If I remember correctly, this is the only information I have about the branch condition. I thought it’s still better than having no condition at all

viper-admin · 2020-02-20T12:28:41Z

@ArquintL commented on 2019-10-01 15:51

Your suggestions are now implemented and conflicts should be fixed

# Conflicts: # src/main/scala/Config.scala # src/main/scala/rules/QuantifiedChunkSupport.scala # src/main/scala/supporters/functions/FunctionVerificationUnit.scala # src/test/scala/PortableSiliconTests.scala

ArquintL added 30 commits May 3, 2019 14:54

initial version for collecting execution time and creating generic re…

0e52a18

…cords

adds export of GenericNode, fixes handling of conditional edges in Sy…

c42481d

…mbEx logger

adds state consolidation logging, improves SymbEx Logger unit tests, …

bdeebdb

…adds logger support for arbitrary CFG branching

fixes more SymbEx Logger unit tests, removes alog files from vc

fcb77d3

adds more sophisticated logger state restoration after branches, adds…

70d1a5a

… checker for exec time completeness on records

fixes SymbExLogger to call collapse for each record

91ee9d8

some cleanup for SymbExLogger modifications

33af6b4

adds incompleteness examples from malte's phd thesis to SymbExLogger …

ee44b9d

…unit tests

adds DeciderAssert record

acb7d2b

adds DeciderAssume records

4b6832c

adds additional records for state consolidation and state merging

477c9cb

adds Retry record when verification failed the first time, a state co…

a52649c

…nsolidation was performed next, and verification is retried

adds silicon cli option 'ignoreAssertTrue'

85f3603

adds local branch record for implies

6fc149f

adapts unit tests to changes for Implies

1dd1018

fixes logger for loops (caused by ignored back edge)

4610344

fixes logging of merge operation in loop out edge, allows multiple re…

1fe8baf

…cords as condition, pre-, or postcondition

replaces 'ignoreAssertTrue' by 'consolidateOnAssertTrue'

09990c7

refactoring and first implementation of new logger using scopes; basi…

c04139b

…cs unit test is working

some refactoring for handling branches, checkers for execution time a…

eb8497f

…nd scoping

branching record is created by brancher, same for joiner, branches ar…

3868037

…e not considered scopes, some runtime checks on logged paths, genericNode export

adds branch info to logger

a4b1543

adds position to GenericNodeData

1be3984

cleans up logger and moves json creation to viperserver

89bf589

Merge changes from viperproject/silicon

117df66

fixes some imports

368ad3c

fixes some imports

c0a7b81

changes package name of SymbExLogger

a0e41dd

adds SMT statistics to logger

aaff230

moves smt solver statistics delta calculations to SymbExLogger

b83655d

fpoli force-pushed the master branch from 5670297 to 76f21ec Compare February 20, 2020 16:01

Merge branch 'master' into arquintl/silicon/default

b6d394c

# Conflicts: # src/main/scala/Config.scala # src/main/scala/rules/QuantifiedChunkSupport.scala # src/main/scala/supporters/functions/FunctionVerificationUnit.scala # src/test/scala/PortableSiliconTests.scala

mschwerhoff merged commit 85ecb64 into master Mar 15, 2020

mschwerhoff deleted the arquintl/silicon/default branch March 15, 2020 12:14

ArquintL mentioned this pull request Jul 6, 2021

Scope-based SymbExLogger Take 2 #562

Merged

Conversation

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

viper-admin commented Feb 20, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants