Abstract Core #28
Merged
Abstract Core #28
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…record, extension_env, and constraints
…g in terms of AbstractInstruction
* cleaned compiler warnings; ported ADD instruction * formatting Co-authored-by: Tannr <tannr@hey.com>
* more concrete instructions; removed prev val from mem op
Made return type for AbstractInstruction abstract. Because instructions can now return different types, the `InnerInterpreter` trait constrains the set of possible return types from individual instructions. All existing instructions still return `AbstractExecRecord`. All existing instructions are concrete so they return `ConcreteAbstractExecRecord` which has its constraint type parameter set to the unit type. This allows concrete instructions to not have any generic type for constraints while still using the same `AbstractExecRecord` return type. Separated AbstractMachine into AbstractMachine, InnerInterpreter, and OuterInterpreter. AbstractMachine - purely encapsulates the current state of the machine. It does not include constraints as concrete machines do not have constraints. InnerInterpreter - handles the return value and state update from execution of an individual instruction. We have two example inner interpreters. The concrete inner interpreter maps simply updates the current machine state. The symbolic inner interpreter returns a vec of new machine states and constraints. OuterInterpreter - handles orchestration of which machine state(s) to run. For the example outer interpreters we implement, we embed the inner interpreter in the outer interpreter struct as a trait object. This allows for some flexibility in choosing different inner interpreters so long as they have a step function of the right type for the outer interpreter. The concrete outer interpreter just steps the concrete inner interpreter until the machine can’t execute any further. The symbolic outer interpreter performs DFS on the search graph of machine states. Note that this architecture allows us to substitute out an alternative symbolic outer interpreter that performs BFS or any other alternative search strategy. I temporarily removed the `PathSummary` portion yet where we use the solver to find the reachable paths and return models. The type signature of `ConcreteOuterInterpreter` is already incredibly complex and I'd prefer to not add the additional generics that the solver is going to entail in a separate PR.
* remove generic from stack
…ilitate custom types support
* remove memory generic * lint
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Decouple core features from convenient features.
Notable differences:
Abstractcomponents are actually well defined data structures that are only abstract over the data types they contain, we have replaced the reliance on type signatures as the primary way to configure a machine with, instead, a "universal" value type that can be lazily interpreted as a different type depending on the intent of the machine author. This dramatically simplifies the type signatures.Configobject that (will in the near future) contain the "hooks" provided bycore::astwhich enable customizing the way in which an abstract value is interpreted by the machine's interpreters.Still TODO:
Abstract-X structures via theirConfigobjectsStackVal,MemValetc., withast::Sentencecore::Constraintnow that both values and constraints can be expressed as sentencesast::Sentence