| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-30 | Executing an actual elf file | Kathy Gray | |
| 2014-09-29 | Connect up to elf model; which doesn't seem to be representing the elf file ↵ | Kathy Gray | |
| properly yet but run_power.native is connected to it | |||
| 2014-09-29 | add run_power to last commit | Kathy Gray | |
| 2014-09-04 | Refine overloading resolution with respect to vectors and ranges | Kathy Gray | |
| Fix a few other bugs as well | |||
| 2014-08-28 | fixes to bugs exposed by arm model | Kathy Gray | |
| 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 | make test_power_interactive working again; now using interp_interface ↵ | Kathy Gray | |
| instead of internal actions | |||
| 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-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-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-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-15 | Add failing test for type of aliases | Gabriel Kerneis | |
| File "test/regbits.sail", line 23, character 3 to line 23, character 4 Type error: Can only assign to identifiers with type register or reg, found identifier CA with type bit | |||
| 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-04 | Correct error of forgetting type information that was allowing more programs ↵ | Kathy Gray | |
| than it should have | |||
| 2014-07-04 | Update power.sail | Gabriel Kerneis | |
| 2014-07-02 | Update Power example | Gabriel Kerneis | |
| 2014-06-27 | Update type conformance for overloading resolution on order arguments. | Kathy Gray | |
| Also, correctly type check nondet blocks | |||
| 2014-06-26 | Adding better support for unspecified values in indexed vectors | Kathy Gray | |
| Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches | |||
| 2014-06-25 | Add support for actions that read just a slice or single bit of a register | Kathy Gray | |
| 2014-06-24 | Get vector length for to_inc_vec and to_dec_vec from the type system after ↵ | Kathy Gray | |
| constraint solving (instead of hardcoding 64 as the default). | |||
| 2014-06-23 | Get indexed vectors, particularly with default values, working | Kathy Gray | |
| 2014-06-18 | Correct effect matching bug; and print out effect lists | Kathy Gray | |
| 2014-06-18 | Make hex constants work; improve utility of casts for selecting overloaded ↵ | Kathy Gray | |
| functions | |||
| 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-09 | Improve interaction after chat with Peter | Gabriel Kerneis | |
| - remember mode (run, step or next) between instructions - display continuation by default in step mode - start in step mode by default - incompatible change: the shorthand for stack is now bt (=backtrace), since s becomes the shorthand for step - incompatible change: pressing enter now repeats the current mode, instead of "step" | |||
| 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-07 | Copy main.bin in Sail repository for Power test | Gabriel Kerneis | |
| 2014-06-07 | Pattern-matching exhaustiveness | Gabriel Kerneis | |
| 2014-06-06 | Add wrapper script and --interactive for demo | Gabriel Kerneis | |
| 2014-06-05 | Shorten debug output for power | Gabriel Kerneis | |
| 2014-06-05 | Enable single-stepping for test/power.sail | Gabriel Kerneis | |
| 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-05-30 | Add pretty-printer test (idempotence) | Gabriel Kerneis | |
| Fails in most cases because of "fresh" variables in type annotations that cannot be parsed again. | |||
| 2014-05-30 | Remove bit-rotted, abonned test file | Gabriel Kerneis | |
| 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-04 | Cosmetic improvements (statistics, --quiet) | Gabriel Kerneis | |
| 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |