| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-01 | Remove old test directory in src/test | Alasdair Armstrong | |
| 2016-10-10 | changed the way registers/register fields work, fixes, nicer names for new ↵ | Christopher Pulte | |
| letbound variables | |||
| 2016-09-21 | fixes | Christopher Pulte | |
| 2016-09-07 | push some lem pp changes | Christopher Pulte | |
| 2016-07-12 | sail-to-lem and lem library fixes | Christopher | |
| 2015-12-21 | fixes, pp progress | Christopher | |
| 2015-12-15 | better location information | Christopher | |
| 2015-11-05 | some progress on lem backend: rewrite away mutable variable assignments, ↵ | Christopher Pulte | |
| rewrite for-loops, if/case-expressions to return updated variables | |||
| 2014-11-27 | updated test for power.sail | Kathy Gray | |
| 2014-11-19 | Correct off-by-one bug in type checking vector slices | Kathy Gray | |
| Convert sparse vectors into full-fledged vectors more frequently and on export to memory system | |||
| 2014-11-12 | Stop overzealously looking for constructors, only when the type suggests to | Kathy Gray | |
| 2014-11-04 | Fixes bugs: | Kathy Gray | |
| not setting starting bit of vector properly not treating properly if when given a non boolean --- bool largely removed in place of bit, removing many/most is_one casts but true and false are still possible values coerces between bit vectors of length one and bits again, because reading from a register can otherwise be wrong with respect to the interface | |||
| 2014-10-22 | Update printing for testing, fix some bugs found along the way | Kathy Gray | |
| 2014-10-16 | bug fixes to run test from Christopher's tests | Kathy Gray | |
| 2014-10-14 | Iron out bugs in running new executable with branching; add new executable ↵ | Kathy Gray | |
| as well. | |||
| 2014-08-27 | Changes to get another (slightly larger) executable running; | Kathy Gray | |
| adding executable as a test as well | |||
| 2014-08-26 | small changes for arm | Kathy Gray | |
| 2014-08-20 | Add ability to track register dependencies in interactive stepper; thus ↵ | Kathy Gray | |
| testing register tracking/tainting | |||
| 2014-08-19 | Add file that actually drives command line interpreter | 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-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-04 | Update power.sail | Gabriel Kerneis | |
| 2014-07-02 | Update Power example | Gabriel Kerneis | |
| 2014-06-11 | power.sail: store mode64bit in a bool register | Gabriel Kerneis | |
| This is now possible because we handle coercions better. | |||
| 2014-06-11 | Update power.sail: remove some hacks | Gabriel Kerneis | |
| 2014-06-07 | Don't use cycle for fetch-decode-execute | Gabriel Kerneis | |
| 2014-06-07 | exts returns bit[64] instead of nat | Gabriel Kerneis | |
| Update power.sail to new, pretty-printer-based version | |||
| 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-06-02 | Fix dependent-type for MEM in power.sail | Gabriel Kerneis | |
| Now, constraint resolution works for test/power.sail | |||
| 2014-04-04 | Improve Power execution | Gabriel Kerneis | |
| - Move FDE loop to the OCaml side of the Power model (avoid leaking memory due to lack of TCO in interpreter) - Display cycle count - Check the value of CIA at the end of each cycle and stop if it is equal to the initial value of LR, returning the value in GPR3. | |||
| 2014-04-03 | Power example now EXECUTES (almost) CORRECTLY! \o/ | Gabriel Kerneis | |
| Warning: we set the link register to the address of the first instruction, which means the program is effectively an infinite loop returning 42 forever. (Except it slows down and leaks memory, probably because the interpreter doesn't optimise the tail call in fde_loop.) 42, 42, 42, 42, 42, 42, 42, 42, ... | |||
| 2014-04-03 | Remove workarounds and update Power model | Gabriel Kerneis | |
| 2014-04-03 | Exhibit two bugs about bitwise operators and vector casts | Gabriel Kerneis | |
| 2014-04-02 | Fix EXTS and signedness of to_num | Gabriel Kerneis | |
| 2014-04-02 | Update Power model | Gabriel Kerneis | |
| 2014-03-20 | Add missing GPR registers for Power example | Gabriel Kerneis | |
| Second instruction now executes (but probably not correctly, check arithmetic since we ignore exts). Next step is to implement bitwise_or. | |||
| 2014-03-20 | Remove work-around from interpreter, move it to power.sail | Gabriel Kerneis | |
| Two bugs are worked-around here: - missing cast to nat when a vector is wrapped in exts (exts is a no-op currently anyway, so we are discarding it) - missing cast (due to limited type-inference) in one if branch: type given explicitly. | |||
| 2014-03-19 | Fetch-decode-execute & init for power | Gabriel Kerneis | |
| 2014-03-13 | Make test_power compiling again | Gabriel Kerneis | |
| 2014-03-11 | More work on interpreter and Power model | Gabriel Kerneis | |
| 2014-03-04 | Minimal power model to run hello world | Gabriel Kerneis | |
| Crashes because register initialization is missing. | |||
| 2014-02-28 | Fetch-decode POWER interpreter | Gabriel Kerneis | |
| Many limitations and bugs currently, but loads binary and decodes opcodes correctly (using endianness hacks). Disabled in the default test suite (but still compiled), run "make test_power" to try it. | |||
| 2014-02-25 | Sensible types for POWER registers | Gabriel Kerneis | |
| 2014-02-12 | More library functions for interpreter | Gabriel Kerneis | |
| There is now enough stuff to decode and execute a very basic Branch instruction (encoding everything as little-endian rather than big- endian among many other work-arounds). | |||
| 2014-02-12 | Fix endianess issues | Gabriel Kerneis | |
| 2014-02-12 | Remove spurious declaration | Gabriel Kerneis | |
| 2014-02-12 | Fix type errors in power.sail | Gabriel Kerneis | |
| 2014-02-07 | Implement is_one | Gabriel Kerneis | |
| 2014-02-07 | Use bit->bool coercion for power.sail | Gabriel Kerneis | |
| 2014-02-05 | Replace symbolic link by actual file | Gabriel Kerneis | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |