Thursday, July 7, 2011

synthesizing specialized hybrid value comparisons with Clojure metasketching

Recall that the hybrid value modifications in the backend extend the notion of a variable-value to be in four states:
  • A known constant (this was the only non-hybrid possibility before)
  • A value less than some bound
  • A value greater than some bound
  • An unknown value
    Things currently aren't very optimized. Suppose we have a variable x in the third state, i.e. we know x >= BND, where BND is some positive constant. Then, if we want to compute x > 0, we should return constant-true, not unknown. Similarly, if we multiply two large values, we should get another large value.

    There's a lot of these specialized functions -- one for every operator, and for every comparator we want to know whether it's possible, or known, that e.g. x > y, or whether is possible, denoted maybe. Instead of writing these core and critical specializations by hand, it would be nice to sketch them.

minor debugging option changes

Sorry I don't have a lot of engineering time, but I changed the debug options for printing phases a little, and the code handling it is a little cleaner than before. Sorry for breaking it in the meantime.

First, the relevant options are, as per the help screen "skdev --help:debug",

    --debug-print-passes   Print names of stages and visitors as they execute
 -p,--debug-dump-after     Stages / visitors to dump the program after (comma-sep)
 -P,--debug-dump-before    Stages / visitors to dump the program before (comma-sep)

Monday, April 11, 2011

Python tprint output

SKETCH now supports generating Python files from tprint output. This is useful for localizing synthesis; for example, extracting a read-write sequence from a concrete scan network, so that one can then synthesize a function for mapping the indices. For a simple example, consider the following sketch, that multiplies [1 .. 4] by a constant value.