Remove the generic from stack. This also requires removing the test where we test when symbolic values are on the stack. We can add that back in when StackVal is the more general Val that uses an ast.

core/instructions/val is being replaced with the core/value module some of the non abstract machine + tests were dependent on the core/instructions/val module so removed those as well

the contrib/tests/simple_lang.rs tests were dependent on core/instructions/val so I removed and replaced with contrib/tests/simple_langg.rs tests

also ran cargo fmt :P

Decouple core features from convenient features.

Notable differences:

1. Since most built in Abstract components 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.
2. Configuration is thus done through a Config object that (will in the near future) contain the "hooks" provided by core::ast which enable customizing the way in which an abstract value is interpreted by the machine's interpreters.

Still TODO:

1. Make use of AST hooks to configure various Abstract-X structures via their Config objects
2. Replace the StackVal, MemVal etc., with ast::Sentence
3. Review the use of core::Constraint now that both values and constraints can be expressed as sentences
4. Review the inner_interpreter-outer_interpreter architecture to integrate its execution with ast::Sentence
5. Bring back the symbolic execution phase of the outer interpreter

…Machine into AbstractMachine, InnerInterpreter, and OuterInterpreter

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 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 SymbolicOuterInterpreter 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.

rebased on top of https://github.com/WilfredTA/symbolic-stack-machines/pull/16

Creates the abstract interface to the constraint solver. Running the symbolic machine now returns

• the model mapping symbolic values to concrete values in the machine
• the symbolic return value of the machine
• the concrete return value of the machine

rebased on top of https://github.com/WilfredTA/symbolic-stack-machines/pull/15

This creates the symbolic machine that wraps a concrete machine. This initial version does not execute the SMT solver and only allows for collecting constraints and splitting the machine state.

rebased on top of https://github.com/WilfredTA/symbolic-stack-machines/pull/14

separating out the core concrete machine into its own trait+implementation

rebased on top of https://github.com/WilfredTA/symbolic-stack-machines/pull/13

Opcode implementations. Opcodes are written so they can be dynamically dispatched to.

rebased on top of https://github.com/WilfredTA/symbolic-stack-machines/pull/12

The separate concrete and symbolic instruction allows for clean interfaces and opcode implementations.

concrete instructions

• only operate on concrete machine state

symbolic instructions

• operate on concrete machine state
• can split into multiple machine states
• can add path constraints

This gives the nice ability to define both concrete and symbolic implementations of the same opcode. I.e. see {concrete, symbolic} JUMPI.

https://github.com/WilfredTA/symbolic-stack-machines/blob/aec8aa99c2c0c19370f8402c3976a41300ed8f70/src/instructions/sym.rs#L12-L48

https://github.com/WilfredTA/symbolic-stack-machines/blob/aec8aa99c2c0c19370f8402c3976a41300ed8f70/src/instructions/misc.rs#L47-L71

The concrete machine will only use the concrete instructions. The symbolic machine will use the hybrid instructions.

this is rebased on https://github.com/WilfredTA/symbolic-stack-machines/pull/11

Adds the ConcreteInt struct which just wraps i64 and implements some of the interfaces the machine needs

This is rebased on top of https://github.com/WilfredTA/symbolic-stack-machines/pull/9 and https://github.com/WilfredTA/symbolic-stack-machines/pull/10

Removing the lifetime from the machine means we have to remove the symbolic context. We'll separate out machines into two separate structs, one that is the concrete machine and a symbolic machine that wraps the concrete machine. So the current machine w/out the lifetime will become the concrete machine.

The two {concrete,symbolic} machines work together with the {concrete,symbolic} instructions. We setup the types so that both machines can take a reference to the same program, but the symbolic machine's job is to make sure that symbolic instructions are never executed by the concrete machine. When they are, the opcode panics.

https://github.com/WilfredTA/symbolic-stack-machines/blob/aec8aa99c2c0c19370f8402c3976a41300ed8f70/src/instructions/mod.rs#L59-L71

https://github.com/WilfredTA/symbolic-stack-machines/blob/aec8aa99c2c0c19370f8402c3976a41300ed8f70/src/machine/symbolic.rs#L65-L106

The symbolic machine will hold a list of constraints but again the constraints will be abstract and not have the lifetime.

In a previous version of symbolic-stack-machines (SSM), each modular component (memory, stack, etc) were all generic over Instruction. The idea was to use Rust's type system to configure the machine's behavior. This turned out to be detrimental to the library's ease of use & ergonomics more specifically.

While climbing out of the so-called "generics-hell", we realized that most of the generics in various components were due to being generic over the type of values stored in the stack, memory, storage, etc. Thus, we created a universal value type that is lazily evaluated; the universal value is actually an AST.

We also introduced a Configuration object for each modular component (StackConfig, MemConfig, etc). These config objects are meant to receive hooks which can be passed to the universal value's AST interpreter. This allows us to treat the universal value in Rust's type system as a single type (thereby drastically simplifying the library's API), while also allowing various components to customize the semantics of that type and specialize it to whichever type is relevant for that component. In other words, it gives us polymorphism across different components as well as polymorphism across different values within a particular component, since the hooks passed to the universal value's interpreter can conditionally evaluate the value as a different type based on the component's state.

The only component that does in fact need to be generic is the ExtEnv. This is because it is meant to be a catch all extension mechanism for implementing symbolic machines with more components, as well as those with bespoke features (e.g., the concept of "gas" in the EVM). Notably, the ExtEnv can also be leveraged to construct register-based machines. The crucial difference between the extension environment component and other components is that it does not have a predefined structure. While other components are well defined though generic over the relevant values on which they operate (a memory is treated as a flat array with some index set and value set; a stack is an abstract data type with API to push, pop, and peek), the ExtEnv has no predefined API nor structural constraints. Thus, we should re-introduce generics to the definition of this component.