| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Again, this is necessary to compare big_int
|
|
constraints. Clean up Lem output a little for readability while debugging.
|
|
|
|
|
|
to_num and to_vec probably still need to be fixed
|
|
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.
|
|
This patch should be reverted when the interpreter is fixed.
The first instruction of main.bin is now executed. The second
one fails, seemingly because of a similar missing cast issue
(external function add receives register GPR1 as value).
|
|
|
|
|
|
|
|
In fact, increasing order is big-endian, not little-endian.
This is good news for us, because it means we do not need any
switch for the POWER spec.
|
|
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.
|
|
Lem's word library does some dark magic because of its assumption that
words represent signed integers. Therefore, it is unreliable to truncate
words, as well as to use the internal representation. boolListFrombitSeq
seems safe for our purposes, though (provided the bitseq has been
created with an infinite length from a positive integer).
|
|
ast, and extending the interpreter to expect annotations.
Annotations and locations are still not used by the interpreter.
|
|
|
|
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).
|
|
|
|
|
|
|
|
Only chapter about branches (except system calls because of sail
typechecking issue). Decoding seems to work. Execution typechecks
currently, but is pretty surely broken otherwise.
|
|
Notice the need for double parentheses in test/test3.sail, because the
interpreter does not perform curryfication automatically (only the first
parameter in kept with List_extra.head):
add ((1, 3)) (* works *)
add (1, 3) (* fails, equivalent to: add (1) *)
Fortunately enough, infix functions work correctly by default. A dirty
quickfix would be easy, but I'm not sure at which level this should be
addressed properly (interpreter? typing? etc.).
|
|
|
|
Tests compile and run properly. There is a lot of hackery going
on to workaround the rough edges of new Lem. Use at your own
risk (you need the "library-format" branch of lem).
|
|
|
