Send simplified list of locations to front end for purposes of providing constraints

[danmatichuk]

In lieu of the full generality of an expression language as described in #425, we can consider a simplified approach where we simply extract a list of "interesting" machine locations from a given trace and assign them to opaque identifiers. The idea is that only these identifiers are sent to the front end and send back to the verifier, which avoids the complexity of passing arbitrary expressions back and forth.

The verifier therefore provides the front end with a list of 4-tuples: the abstract identifier, the symbolic expression, the concretized expression with respect to the current trace, and the type

[lcasburn]

From @danmatichuk:

Implementation steps needed to address this issue:

1. Create hook to tell verifier to regenerate trace using constraint. Done when verifier can correctly pause and continue from that point without issue.
   • Add menu item to trace
   • Add new event type so Scheduler can pause and wait for user input for constraint
2. Implement What4 builder to emit identifiers rather than formal symbolic terms.
3. Serialize trace and sent list of MemOp expressions to UI
4. Receive constraint on identifier from UI.
5. Deserialize identifier to retrieve formal term to apply to constraint.
6. Assert constraint
7. Test by manually constructing json constraint input expected from UI

[lcasburn]

From @danmatichuk:

• Prioritized step (2) to get sample data to @jim-carciofini faster. Realized we don't need power full What4 builder. Added configuration parameter to serialization monad to permit switching modes between identifier or formal symbolic terms.
• Step (3) needs full trace to be flattened into list of memory operations. Extract reads from concrete addresses only because rendering symbolic address is not needed for SCADA example. Have written code that extracts the memory reads (ie. traceFootprint).
• Step (4); also have generated mapping to identifiers and can map identifiers back to expressions. Need input from @jim-carciofini before getting step 4 working end to end.
• Expect to have trace information ready today from step (3). Then jumping back to step (1).

[jim-carciofini]

My plan is to implement a GUI for a limited form of constraint for now. Basically a conjunction of relations with LHS a variable and RHS and integer constant. The relations I will allow are: LTs | LTu | GTs | GTu | LEs | LEu | GEs | GEu | NEQ | EQ. We can allow more general constraints on the option if desired.

Here is a sketch of the JSON I could send to the verifier:

{"kind": "trace-constraint",
 "id": "trace_id",
 "constraint": {"kind": "operator",
                "operator": "And",
                "operands": [
                  {"kind": "operator",
                   "operator": "rel_1", 
                   "operands:" [
                      {"kind": "variable", "id": "var_1_id"},
                      {"kind": "integer", "value": "const_1"}]},
                  ...]}

Seem reasonable? Nothing set in stone yet.

[danmatichuk]

I have a work in progress pr #428 that adds a footprint for the original and patched traces. The format is the same as the register and memory events that are sent with the concrete traces, but the values are either concrete (as with a concrete trace) or be symbolic identifiers that look like this:

{ "symbolic_ident" : "12345", "type" : "(BV 8)" }

For an 8-bit bitvector.

[jim-carciofini]

Is the "symbolic_ident" appropriate to show the user and to identify the symbolic identifier in the constraint I send to the verifier?

[jim-carciofini]

Is the PR stable enough for me to try it?

[lcasburn]

From @danmatichuk:

Step (2) & (3) implemented. Working on step (1) "Create hook to tell verifier to regenerate trace using constraint." Have plumbing in place for receiving constraints, plan for today is to create the constraint events by adding these features:

• Add global state to verifier, a map that identifies which traces are waiting for constraints.
• Front end will need to send a request to tell the verifier to regenerate the trace.
• Function tells verifier when it encounters trace again, to stop and prompt user for constraints

[jim-carciofini]

Have you started coding to the JSON structure of constraints I specified above? It occurred to me that we could save ourselves some busy work and I can just send the constraints as a simple list of triples [, , ] with being the same JSON for a var that you sent me. We can generalize this if desired on the option.

[danmatichuk]

I'm just starting this now so any format is fine. The main thing I need in addition to the triple is a mapping to the corresponding trace. At the moment probably the easiest way to do it is to just take a list of list of triples, and just assume by convention that they're in the same order as the trace footprints.

[danmatichuk]

For simplicity we're restricting the cases where you can generate new traces to only the traces presented at the end of the analysis for each equivalence condition.

This simplifies the interaction model significantly, since the trace generation can be easily made re-entrant during this final phase (since we know the assumptions/domain for each node is now fixed). Later we can generalize this to allow providing constraints to any of the traces emitted as part of the analysis, which just requires a bit more coordination between the front and backend in order for the user to request nodes to be re-processed with extra constraints.