| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This should fix the issue raised in commit 45554f
Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations
|
|
functions in mips spec in prepartion for using this file in mips prelude. Also modify tests that use this header. We should consider prefixing library builtins to avoid name clashes. overload can then be used to provide aliases if desired.
|
|
Also fixes to C backend for compiling MIPS spec to C
- Fix an issue with const correctness in internal_vector_update
functions generated by C backend
- Add builtins for MIPS to sail.h
- Fix an issue where reg_deref didn't work when called on pointers to
large bitvectors, i.e. vectors containing references to large
bitfields as in the MIPS TLB code
- Various bug fixes and changes for running U-boot on ARM model,
including for interpreter and OCaml compilation.
- Fix memory leak issues and incorrect shadowing for foreach loops
- Update C header file. Fixes memory leak in memory read/write
builtins.
- Add aux constructor to ANF representation to hold environment
information.
- Fix undefined behavior caused by optimisation left shifting uint64_t
vectors 64 or more times. Unfortunately there's more issues because
the same happens for X >> 64 right shifts. It would make sense for
this to be zero, because that would guarantee the property that ((X
>> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n -
1) >> 1) in the optimisation to ensure that we don't cause
UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64
in one go isn't according to the C standard. This issue with
right-shifts only occurs for zero-length vectors, so it's not a huge
deal, but it's still annoying.
- Add versions of print_bits and print_int that print to
stderr. Follows OCaml convention of print/prerr. Should make things
more explicit. Different backends had different ideas about where
print should output to, not every backend needs to have this
(e.g. theorem prover backends don't need to print) but having both
stderr and stdout seperate and clear is useful for executable models
(UART needs to be stdout, debug messages should be stderr).
|
|
This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in
```
val f : nat -> nat
let x = f(3)
```
whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.
Also:
- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
pass didn't add type paramemters for newly added type variables in
generated function parameters.
- Updated string_of_ functions in ast_util to reflect syntax changes
- Fixed a C compilation issue where elements of union type
constructors were not being coerced between big integers and 64-bit
integers where appropriate
- Type annotations in patterns now generalise, rather than restrict
the type of the pattern. This should be safer and easier to handle
in the various backends. I don't think any code we had was relying
on this behaviour anyway.
- Add inequality operator to lib/flow.sail
- Fix an issue whereby top-level let bindings with annotations were
checked incorrectly
|
|
First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.
Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.
Finally support for vector literals that are non-bitvectors has been
added.
|
|
Comment out partially working optimisation passes for now
|
|
Fixed an issue whereby an option constructor that was never
constructed, but only matched on, would cause compilation to
fail. Temporarily fixed an issue where union types that can be
entirely stack-allocated were not being treated as such, by simply
heap-allocating all unions. Need to adapt the code generator to handle
this case properly. Fixed a further small issue whereby multiple union
types would confuse the type specialisation pass.
Added a test case for compiling option types.
RISCV now generates C code, but there are still some bugs that need to
be squashed before it compile and work.
|
|
Add a flag to Sail that allows for an image of an elf file to be
dumped in a simple format using linksem, used as
sail -elf test.elf -o test.bin
This image file can then be used by a compiled C version of a sail
spec as with ocaml simply by
./a.out test.bin
|
|
Previously union types could have no-argument constructors, for
example the option type was previously:
union option ('a : Type) = {
Some : 'a,
None
}
Now every union constructor must have a type, so option becomes:
union option ('a : Type) = {
Some : 'a,
None : unit
}
The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.
This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:
function is_none opt = match opt {
Some(_) => false,
None => true
}
it is now matched as
function is_none opt = match opt {
Some(_) => false,
None() => true
}
note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.
There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.
The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using
$include <option.sail>
|
|
Fix some issues where some early returns in functions would cause
memory leaks, and optimize struct updates so the struct is not copied
uneccesarily.
Also make C print_bits match ocaml version output, and update tests.
|
|
|
|
Fixed an issue with pattern matching on enums
Fixed an issue whereby fix_early_returns would cause memory leaks
Added optimizations for some of the builtins used in the decode
function. Optimizations are turned on with the -O flag.
|
|
Add support for short-ciruiting and/or. I forgot about this in the
original ANF specification and not having it causes problems for the
ARM spec.
|
|
Now compiles to C and builds a working executable. Just need to
correctly implement all the library builtins (some are still stubs),
and it should work.
|
|
|
|
Goes through the C compiler without any errors, but as we still don't
have all the requisite builtins it won't actually produce an
executable. There are still a few things that don't work properly,
such as vectors of non-bit types - but once those are fixed and the
Sail library is implemented fully it should work.
|
|
|
|
|
|
|
|
|
