Remove SymbolOrAliasSorts #392

ttuegel · 2018-12-19T20:29:50Z

Remove SymbolOrAliasSorts from MetadataTools.

Removes modules Kore.ASTUtils.SmartConstructors and Kore.ASTUtils.SmartPatterns. New constructors and pattern synonyms for verified patterns reside in Kore.AST.Valid with helpers defined in Kore.AST.Lens.

Reviewer checklist

Test coverage: stack test --coverage
Public API documentation: stack haddock
Style conformance: stylish-haskell

virgil-serbanuta

Thanks for doing this, each time I wrote give sortTools I thought how nice it could be with annotations!

You said that there was some fragile code that dealt with sorts. If there aren't many instances, could you add todos for all of them, explaining the issue (with my name, unless you want to fix them)? If there are many instances, could you add a few TODOS for places that are good examples for these issues, mentioning that all similar instances must be fixed?

@traiansf I didn't have time to look at things under kore/test, you should keep that in mind when reviewing.

src/main/haskell/kore/src/Kore/AST/Kore.hs

src/main/haskell/kore/src/Kore/AST/Lens.hs

src/main/haskell/kore/src/Kore/AST/Pure.hs

virgil-serbanuta · 2018-12-20T08:53:27Z

src/main/haskell/kore/src/Kore/Parser/ParserImpl.hs

@@ -459,13 +459,13 @@ BNF definitions:
 @
 ⟨variable⟩ ::= ⟨object-variable⟩ | ⟨meta-variable⟩
 @
-unifiedVariableParser :: Parser (UnifiedVariable Variable)
+-}
+unifiedVariableParser :: Parser (Unified Variable)


This is not used anywhere, right? @traiansf Do you remember why we have this? Is it worth keeping?

If nobody can come up with a reason for keeping it, I think we should delete this function.

I think that we originally though we might need it, and it somehow seemed to fit into the overall parsing picture; if it's not used, we should drop it; it's not hard to write it again if we decide it's useful later.

It's used in the Unparse tests to check that we can correctly do the parsing-unparsing round-trip.

src/main/haskell/kore/src/Kore/Predicate/Predicate.hs

src/main/haskell/kore/src/Kore/Step/BaseStep.hs

virgil-serbanuta · 2018-12-20T09:32:50Z

src/main/haskell/kore/src/Kore/Step/Simplification/Ceil.hs

        , Ord (variable level)
+        , Show (variable level)


Could we group these two constraints into a single one, DebugVariable or something similar (not necessarily in this PR)? I guess that's their purpose, so we should be explicit about what happens.

Yes, I will make a separate pull request for that. I think it should be a class for any syntactic object, not just variables; the Unparse (variable level) is just getting pulled in to satisfy an Unparse (Pattern level domain variable child) instance somewhere. But at this location, the constraint could just be DebugSyntax (variable level).

virgil-serbanuta · 2018-12-20T09:37:58Z

src/main/haskell/kore/src/Kore/Step/Simplification/Ceil.hs

+            in
+                (result, SimplificationProof)
+          where
+            Application { applicationSymbolOrAlias = patternHead } = app


I'm starting to like this way of extracting field values.

virgil-serbanuta · 2018-12-20T10:01:53Z

Oh, one more thing: if I remember correctly, you said that you expected some performance improvement. It would be nice if that information would be present in the PR description and if it would preserved in the commit history after merging.

eviefp · 2018-12-20T10:24:50Z

It would be even nicer if we could somehow use Jenkins to time at least the integration suite and export the data somewhere, to generate a report. Now that I think about it, would be interesting to also track coverage and docs.

traiansf

Tests look OK to me. I'll leave the final approve to @virgil-serbanuta

The sort `predicateSort` is renamed to `_PREDICATE{}`; the underscore makes it an invalid identifier in the concrete syntax of Kore. The definition verifier now ensures that it is not defined, just to be pedantic.

Types `Module` and `Definition` are now parameterized by sentence type and gain instances `Functor`, `Foldable`, and `Traversable`.

Add `eraseSentenceAnnotations` to erase annotations from pure `Sentence`s and `eraseUnifiedSentenceAnnotations` to erase annatations from `UnifiedSentence`s.

The function `renderDefault` is a helper for writing error messages. The functions `parameters`, `arguments`, and `attributes` are useful for writing instances of `Unparse`.

Unlike `Kore.ASTHelpers.substituteSortVariables`, this function does not fail if a sort variable is not found.

The new module Kore.AST.Valid implements constructors and patterns for valid pure Kore syntax trees.

`extract` is a well-known name used by the `Comonad` class. As we use `Comonad` more, this name will collide.

`Control.Comonad` is part of the intended interface of the `PurePattern` type.

The `HasCallStack` constraint causes the error message to appear where `testSymbolWithSolver` is called.

ttuegel · 2018-12-20T22:04:24Z

@virgil-serbanuta This is ready for re-review now. I will have performance numbers tomorrow, but I would expect < 5% change from this. SymbolOrAliasSorts was the cheapest lookup in MetadataTools. The biggest gains will come from attribute annotations, but I started with sort annotations because I think that is easier.

virgil-serbanuta

I've added a new comment in this review round, and you still have two from the previous round: the parser one and the performance stats one. I'm not going to insist on the last one if you think it does not make sense.

src/main/haskell/kore/src/Kore/AST/Lens.hs

Type SymbolOrAliasSorts and the MetadataTools field symbolOrAliasSorts are not necessary with pattern sort annotations. Concrete execution time decreases by 6% for IMP programs, but languages with larger definitions may see greater improvement because the complexity of sort lookup is reduced from logarithmic (in the number of defined symbols) to constant-time.

`translatePredicate` attempts the following, in order, to translate the children of an `\equals` predicate: 1. Translate children as builtin domain value patterns. 2. Translate children as predicates. 3. Translate the entire predicate uninterpreted. We always attempt translation as builtin domain value patterns first because that is most specific. We cannot use the sorts alone to choose between translating as builtin domain value patterns or predicates, because predicates can occur in any sort.

Specifying all class functions for these instances for `PurePattern` and `KorePattern` allows us to take advantage of specialized implementations in the parent instances. (I originally wrote this patch when I was on a performance wild-goose chase. In the end, this is worth less than 0.5% on performance, but I wasn't going to throw it away.)

Functions bottomOf and topOf create a \bottom or \top expanded pattern of a given sort.

Function mkSortVariable constructs a sort variable with the given name, the analog of function mkSort, which constructs an actual sort.

The search command now uses forceSort to coerce its result into the sort of the original configuration pattern. The prove command uses mkSortVariable to construct a dummy sort variable if the sort of the result is flexible.

Fixes runtimeverification/hs-backend-booster#373 This PR makes `kore-rpc-booster` return `"execute"` responses with `"reason": "aborted"` in cases when Kore's simplifier fails due to `DecidePredicateUnknown` in the post-exec simplification in `Proxy.hs`. **Scenario before** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> JsonRpcError` ``` returning `JsonRpcError` resulted in loosing information gained by executing in booster for X steps + in kore for up to 1 step. **Scenario now** ``` "execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> ExecuteResult {reason=Aborted, unknownPredicate = <predicate>}` ``` this this change, we return the reached state (may be branching) and do not lose information anymore. Additionaly, we return the unknown predicate, so that `pyk` can decide what to do with these. PR to `pyk` that takes advantage of this feature by intrroducing `Undecided` nodes to KCFG: runtimeverification/pyk#744 --------- Co-authored-by: Samuel Balco <[email protected]> Co-authored-by: github-actions <[email protected]> Co-authored-by: rv-jenkins <[email protected]>

ttuegel requested review from traiansf and virgil-serbanuta December 19, 2018 20:29

ttuegel force-pushed the remove-symbol-or-alias-sorts branch from 7a49019 to 4be8c8f Compare December 19, 2018 20:34

virgil-serbanuta reviewed Dec 20, 2018

View reviewed changes

traiansf reviewed Dec 20, 2018

View reviewed changes

ttuegel force-pushed the remove-symbol-or-alias-sorts branch from 4be8c8f to ebbbd09 Compare December 20, 2018 19:37

ttuegel and others added 15 commits December 20, 2018 15:19

SmartConstructors: Make predicateSort unrepresentable in Kore

98a7dd5

The sort `predicateSort` is renamed to `_PREDICATE{}`; the underscore makes it an invalid identifier in the concrete syntax of Kore. The definition verifier now ensures that it is not defined, just to be pedantic.

Kore.AST.Pure: Add eraseAnnotations

7bcaaf6

Kore.AST.Pure: Generalize type of asConcretePurePattern

49a2f45

Sentence: Add instances Functor, Foldable, and Traversable

e7d30bc

Types `Module` and `Definition` are now parameterized by sentence type and gain instances `Functor`, `Foldable`, and `Traversable`.

Sentence: Add VerifiedKoreModule and VerifiedKoreDefinition

3c884eb

Sentence: Add eraseSentenceAnnotations

8218da5

Add `eraseSentenceAnnotations` to erase annotations from pure `Sentence`s and `eraseUnifiedSentenceAnnotations` to erase annatations from `UnifiedSentence`s.

AxiomPatterns: Remove syntactically-invalid test

69244cc

Kore.Unparser: Export helpers

a0bad3f

The function `renderDefault` is a helper for writing error messages. The functions `parameters`, `arguments`, and `attributes` are useful for writing instances of `Unparse`.

Kore.Sort: Add substituteSortVariables

3bc798f

Unlike `Kore.ASTHelpers.substituteSortVariables`, this function does not fail if a sort variable is not found.

Add module Kore.AST.Valid

18fb43e

The new module Kore.AST.Valid implements constructors and patterns for valid pure Kore syntax trees.

OrOfExpandedPattern: Rename extract to getMultiOr

7c3a98c

`extract` is a well-known name used by the `Comonad` class. As we use `Comonad` more, this name will collide.

Kore.AST.Pure: Re-export Control.Comonad

c38d29b

`Control.Comonad` is part of the intended interface of the `PurePattern` type.

Kore.AST.Sentence: Add VerifiedPureSentence

3f8c557

Test.Kore.Comparators: Add instances for Valid

f6748f5

testSymbolWithSolver: Add constraint HasCallStack

58bc4ad

The `HasCallStack` constraint causes the error message to appear where `testSymbolWithSolver` is called.

ttuegel force-pushed the remove-symbol-or-alias-sorts branch from ebbbd09 to e40ea73 Compare December 20, 2018 22:01

virgil-serbanuta approved these changes Dec 21, 2018

View reviewed changes

src/main/haskell/kore/src/Kore/AST/Lens.hs Outdated Show resolved Hide resolved

ttuegel added 4 commits December 21, 2018 11:51

Kore.Predicate.Predicate: Add instance Unparse GenericPredicate

80a751d

MockMetadataTools: Add HasCallStack constraints

293668b

ttuegel force-pushed the remove-symbol-or-alias-sorts branch from e40ea73 to 4390f7d Compare December 21, 2018 17:51

ttuegel added 2 commits December 21, 2018 15:00

Kore.Step.ExpandedPattern: Add bottomOf and topOf

22ac134

Functions bottomOf and topOf create a \bottom or \top expanded pattern of a given sort.

Kore.AST.Valid: Add mkSortVariable

d5949b1

Function mkSortVariable constructs a sort variable with the given name, the analog of function mkSort, which constructs an actual sort.

ttuegel force-pushed the remove-symbol-or-alias-sorts branch from 4390f7d to 280be68 Compare December 21, 2018 21:00

ttuegel added 2 commits December 21, 2018 15:23

kore-exec: Output a properly-sorted pattern

2de5854

The search command now uses forceSort to coerce its result into the sort of the original configuration pattern. The prove command uses mkSortVariable to construct a dummy sort variable if the sort of the result is flexible.

TODO: Preserve pattern sorts in the simplifier

4700c69

ttuegel force-pushed the remove-symbol-or-alias-sorts branch from 280be68 to 4700c69 Compare December 21, 2018 21:23

ttuegel merged commit 8210f59 into runtimeverification:master Dec 21, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Remove SymbolOrAliasSorts #392

Remove SymbolOrAliasSorts #392

ttuegel commented Dec 19, 2018

virgil-serbanuta left a comment

virgil-serbanuta Dec 20, 2018

traiansf Dec 20, 2018

ttuegel Dec 21, 2018

virgil-serbanuta Dec 20, 2018

ttuegel Dec 21, 2018

virgil-serbanuta Dec 20, 2018

virgil-serbanuta commented Dec 20, 2018

eviefp commented Dec 20, 2018

traiansf left a comment

ttuegel commented Dec 20, 2018

virgil-serbanuta left a comment

Remove SymbolOrAliasSorts #392

Remove SymbolOrAliasSorts #392

Conversation

ttuegel commented Dec 19, 2018

Reviewer checklist

virgil-serbanuta left a comment

Choose a reason for hiding this comment

virgil-serbanuta Dec 20, 2018

Choose a reason for hiding this comment

traiansf Dec 20, 2018

Choose a reason for hiding this comment

ttuegel Dec 21, 2018

Choose a reason for hiding this comment

virgil-serbanuta Dec 20, 2018

Choose a reason for hiding this comment

ttuegel Dec 21, 2018

Choose a reason for hiding this comment

virgil-serbanuta Dec 20, 2018

Choose a reason for hiding this comment

virgil-serbanuta commented Dec 20, 2018

eviefp commented Dec 20, 2018

traiansf left a comment

Choose a reason for hiding this comment

ttuegel commented Dec 20, 2018

virgil-serbanuta left a comment

Choose a reason for hiding this comment