| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-16 | bug fixes to run test from Christopher's tests | Kathy Gray | |
| 2014-10-07 | Connect interpreter to representation of instructions. | Kathy Gray | |
| Warning: this changes a few of the constructor names in the instruction_extractor.lem interface | |||
| 2014-10-07 | Put in type for instruction form for models; remove extra information from ↵ | Kathy Gray | |
| Bytevectors; add place holder for memory size dependency tracking | |||
| 2014-09-04 | Make exhaust run from the first breakpoint in the interactive interpreter | Kathy Gray | |
| (I still think this is a silly place to run exhaust from, but it no longer finds errors or crashes) | |||
| 2014-08-26 | small changes for arm | Kathy Gray | |
| 2014-08-21 | Improve printing of function calls in stepper mode | Kathy Gray | |
| 2014-08-18 | Handling many register reads, writes, and memory reads. | Kathy Gray | |
| There are problems that warrant discussion about handling special registers that hold records or data structures previously. | |||
| 2014-08-18 | Switch run_power to use interp_interface. Compilers and begins running, and ↵ | Kathy Gray | |
| then hits an error. So still in progress Note: moved barrier kind changes to interp_interface, along with other memory kinds | |||
| 2014-08-18 | tweak barrier kinds in interface (likely needs changes elsewhere) | Peter Sewell | |
| 2014-08-13 | FInd/fix a redundant case now that warnings are manageable | Kathy Gray | |
| 2014-08-12 | taint tracking through most of interpreter | Kathy Gray | |
| Need to add cases for tracking a taint past a conditional check where possible; and then to actually generate them from reading registers. | |||
| 2014-08-12 | more taint tracking, yet again | Kathy Gray | |
| 2014-08-11 | More taint tracking. | Kathy Gray | |
| Catch interp_inter_imp up with interp. WARNING: This commit triggers an exponential performance bug in Lem. To alleviate this bug, I am running with a locally modified Lem that has line 1321 of lem/src/typed_ast.ml commented out (On my laptop, I gave up trying to compile after about 900 seconds; beefier computers May be able to run unmodified, I don't know) | |||
| 2014-08-09 | More tracking register dependency; another check point that compiles in ↵ | Kathy Gray | |
| under two minutes | |||
| 2014-08-08 | Tracking register dependence. | Kathy Gray | |
| Check point where Lem will compile interpreter in under 2 minutes | |||
| 2014-08-07 | Fix bug introduced by last commit | Kathy Gray | |
| 2014-08-07 | Track taints across machine calls. | Kathy Gray | |
| This introduced a bug in vector.sail, commented out and needs to be fixed. | |||
| 2014-08-05 | start tainting values with register dependencies | Kathy Gray | |
| 2014-08-01 | Support separated memory read/write functions. | Kathy Gray | |
| Also allows register writing functions to be on the left hand side of an assignment in the same way. The last parameter to a writing function is the value to be written, and should appear on the right hand side of an assignment expression. | |||
| 2014-07-30 | working dec vectors | Kathy Gray | |
| 2014-07-18 | Writing to concatenated aliases | Kathy Gray | |
| 2014-07-16 | Reading from an alias to two concatenated registers; not writing yet. | Kathy Gray | |
| 2014-07-16 | Get writing working for aliases in the interpreter, other than concatenation. | Kathy Gray | |
| 2014-07-14 | Add register to alias concatenation type | Kathy Gray | |
| 2014-07-14 | Initial support for aliases and exit through the type system and the ↵ | Kathy Gray | |
| interpreter. An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter. | |||
| 2014-07-03 | Adjust behavior on Unknown values in pattern match to stop matching as soon ↵ | Kathy Gray | |
| as a pattern is matched without using an unknown; also causes full expansion on function calls with unknowns matched in patterns, however the local state is not reset. | |||
| 2014-07-02 | Fix ordering issue in vector-concat pattern matching | Gabriel Kerneis | |
| 2014-06-30 | Support for nondeterministic blocks | Kathy Gray | |
| 2014-06-25 | Add support for memory barrier | Kathy Gray | |
| 2014-06-25 | Add support for actions that read just a slice or single bit of a register | Kathy Gray | |
| 2014-06-24 | Get enumerations working in interpreter | Kathy Gray | |
| (plus a few other small related corrections) | |||
| 2014-06-23 | Get indexed vectors, particularly with default values, working | Kathy Gray | |
| 2014-06-18 | Make hex constants work; improve utility of casts for selecting overloaded ↵ | Kathy Gray | |
| functions | |||
| 2014-06-12 | Interpret when an unknown is inserted into the program by interp_exhaustive | Kathy Gray | |
| Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet. If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables. In a function call, the cases are all collected but the support is not in place at the moment to evaluate them. If an unknown is the result of the cond expression in an if, the then and else case become a block. Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet. | |||
| 2014-06-09 | Add more stops in interpreter (stopping just at the point of each internal ↵ | Kathy Gray | |
| function call) Also turning off an annoying printf I left in. | |||
| 2014-06-09 | Working towards evaluating with interp_exhaustive | Kathy Gray | |
| 2014-06-04 | Fixup type coercions and overloading | Kathy Gray | |
| Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions. Warning: test_power does not run as not all overloaded funcitons are implemented Warning: vector concatenation does not pretty print to sail source yet | |||
| 2014-05-28 | Support stepped interpreting, and use normalisation instead of eval_nexp in ↵ | Kathy Gray | |
| constraints | |||
| 2014-05-21 | More interface support; interp_inter_imp now compiling | Kathy Gray | |
| 2014-05-20 | Fix interp compiling bug | Kathy Gray | |
| 2014-05-12 | More interface support | Kathy Gray | |
| 2014-05-08 | more interface changes | Kathy Gray | |
| 2014-05-06 | Begin tie to ppcmem style actions/outcomes | Kathy Gray | |
| Change type of + on vectors to (bit vector,bit vector) -> bit vector | |||
| 2014-04-25 | rename interpreter's local memory type to reflect that it's all local memory | Kathy Gray | |
| 2014-04-21 | Remove unsoundness of pattern match in interpreter | Kathy Gray | |
| 2014-04-15 | Use type information in vector concatenation pattern matching in interpreter. | Kathy Gray | |
| Does not properly bind variables (i.e. in the pattern 0b01:(bit[3]) a: 0b0001 subsequent uses of a will not be bound in the interpreter, though they are in the type checker), so until bug is fixed, treat all such identifiers as _ | |||
| 2014-04-08 | Reduce redundant information in AST | Kathy Gray | |
| 2014-04-03 | Re-index vector slices | Gabriel Kerneis | |
| - increasing vector slices are re-indexed from 0 - decreasing vector slices are re-indexed towards 0 I don't know how the type system handles this currently, but it is essential for the correctness of execution. | |||
| 2014-04-03 | Typeclass Eq for values | Gabriel Kerneis | |
| Again, this is necessary to compare big_int | |||
| 2014-04-02 | Solve more constraints; fix up test suite bugs uncovered by solving more ↵ | Kathy Gray | |
| constraints. Clean up Lem output a little for readability while debugging. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |