ucsd-pl / inv-gen-game Goto Github PK

Code in game_graph.ts responsible for building CFG from boogie level cannot yet handle branches in loops correctly (those seem like multiple looping paths). This exhibits as an exception in the browser while loading a new level.

JS semantics differ from boogie, z3, and sanity when evaluating (-1 mod *). For example
(-1 mod 3) evaluates to -1 in JS, and to 2 in boogie/z3. This is a big problem for mod levels. May need a different evaluation scheme in the frontend

Currently our database is a single sqlite file per experiment. As you can have multiple servers running at the same time in an experiment (when you pulished multiple hits at the same time) you can have concurrent accesses to the database. This can lead to corruption. Options include:

1. For now only run 1 hit at a time for experiment
2. Use a file lock
3. Use an actual db server

The partition: attribute is useful, as it marks the assume statements genreated from if/loop conditionals.
It would be nice to add to the grammar and ast an option to hang attributes around.

JS division is float, whereas boogie division is int. Thus any invariant using division evaluates differently in the UI and in the backend. Need a different evaluation scheme in the UI

Non-deterministic transitions need to be handled in the buildGraph function in game_graph.ts.

List to keep track:
- boogie_eval

We build a lot of redundant And/If levels in the expressions that we generated. Flatten those down for readability

The implementation of loops currently conservatively assumes that the only way to exist a loop is from a single exit node straight from the loop header. This doesn't account for cases such as breaks/gotos out of the loop. For now this is not a problem - marking for future fixes.

Our implementation of loops currently looks at provably feasible paths. As a result, it may miss a loop, if for example it follows another loop, but only executes if the first loop has iterated a number of times.
For now not a problem, as we are dealing mostly with simple single-loop programs. Marking for future fix.

The current implementation looks for entire unrollings from the start repeatedly. Instead it should look for one more unroll starting with the final values of the previous invocation. I.e. try to extend a previous partial state.