Wishlist

Features

• All properties should be able to be turned on or off
• Any function can be an entry point. Something like -programEntry=<function ID>
• CIVL report coverage data
  • Which statements executed and the number of times they were. Perhaps color code the statements.
• CIVL must be concurrent
  • Care should be taken to maintain "debug-ability." In particular, objects which get assigned some sort of ID determined by simply incrementing an integer should be instead assigned a more specific ID (when possible) that won't change between different executions of the same CIVL command. That way we can reliably set breakpoints in our code based on these IDs.
• CIVL debugger
  • Able to manually step through code choosing which transitions to take.
  • Breakpoints
  • Some statement that you can insert that, when in debugging mode, asks which transition to take at that point. $ask;
  • At any stopped point in the code be able to observe the current execution path and state.
  • Similarly, be able to evaluate expressions at any point from any specific process.
• Be able to store high memory items into the hard drive to save memory while executing.
• -showProgram should be able to be directly executed by CIVL.
  • Be able to specify which transformations we apply when executing -showProgram
• If -showProgram enabled and we get an error, then print AST before exiting.
• Be able to specify hardware environment to verify under like ints are 32 bits, floats are 32 bits, big-endian vs little-endian, etc.
• Increased emphasis on static analysis.
• There must be a way to implement malloc without knowing the element type. Possibly, design a heap using $bundles.
• civl verify should return a value in the command line based on the error found (or 0 if no error was found).
• Command line option to generate certain stats about a run (i.e. how many symbolic states occurred at each program location, how much branching occurred at each location, etc).
• Be able to save states to memory (perhaps just at specific program points or when specific conditions hold) and later start CIVL back up from those intermediate states. That way issues that don't occur until deep into the state exploration (perhaps minutes or hours into a search) can be quickly returned to.
• Tool for viewing and filtering explored state space:
  • civl verify would generate a state space file containing all states and transitions it explored (similar to how -showStates and -showTransitions works but just more compactly stored and with some extra metadata).
  • File can be "filtered" to only show states and transitions which reach (or are reachable from) some set of states.
  • Would either be implemented as a GUI for viewing and filtering these files or as a command line tool which takes as input a results file and parameters specifying how to filter the space, and then prints the filtered results.
• Be able to obtain the return value of a function when $spawning it. Currently the return value is ignored if you spawned a process on a function. But maybe we can pass a variable to $spawn that gets filled out with the return value when the process terminates. Then we can access this variable when we know that the process has terminated (i.e. after we $wait on the process).

Design

• Everything goes in one repository
• The ability to associate static traits to ASTs like "no for loops" or "side effect free", etc.
• Be able to easily loop over AST nodes of a certain type (in program order). Maybe just support visitor pattern.
• Make it easy to create custom static analyses, especially fundamental ones like dataflow analysis
• CIVL-C language and library must be completely well-defined and documented.
• CIVL-IR must be completely well-defined and documented.
• Remove StatePredicate abstraction and just check for deadlocks directly in the enabler.
• Break up Evaluator by removing big switch:
  • Have "ExecutableExpression" and "ExecutableStatement"-type classes which have an evaluate method and extend the syntactic Expression and Statement classes.
• Components:
  • Util - uses nothing
  • SARL - uses Util
  • ABC - uses SARL, Util
  • MC - uses ABC, SARL, Util
• Make CIVLType richer, acting as an interpreter for values (symbolic expressions). Each CIVLType should have methods that consume and produce symbolic expressions. For example, each should have a method to cast a value to another (acceptable) type. Each should have a method to create values for that type.
• No more dependent types in SARL. SARL arrays will not have length baked into type. CIVL will simply encode bounded arrays as an unbounded array paired with an integer representing the arrays size. In other words, move the state out of the type and into the value.
• Prefer using static methods and variables over factory objects for object creation and manipulation. Less cruft this way (don't have to pass factories all over the place) and also discourages relying on stateful implementations which are more error prone and harder to debug.
• Easier construction and manipulation of ASTs:
  • All new ASTNodes require a Source object which is very tedious to construct meaningfully. Most of the meaningful info (when creating new ASTNodes in a transformer) is in the String it is constructed with which could just be deduced from the ASTNode itself.
  • ASTNodes are immutable but the structure of an AST overall is not though, requiring the need to manage ownership of ASTNodes which can be hard to get right.

Process

• No additions accepted to trunk until
  1. at least unit tests with 100% statement coverage
  2. the code has been read by at least two other developer
     • Perhaps use some kind of web tool that you can highlight code and leave comments on
• Should be regular formal code reviews
• Most JUnit tests should be focused on one specific class. Currently a large amount of our tests are more like "integration" tests rather than "unit" tests.
• Integration tests running civl verify should be more fine-grained than "assert true" and "assert false." Perhaps utilize the return code suggestion made in the Features section of this list.
• JUnit tests should minimize external prover calls as much as possible because they can cause our testing framework to be unstable:
  • Tests may fail if timeout is too low, and they may take too long if it is too high.
  • External provers get updates which may change their results and hence the results of our tests.
  • Different developers may have different prover versions, causing discrepancies between their test results.

Continue Doing

• Code formatter
• Automatic test and coverage analysis