sail/language, branch sail2 Formal specification language for ISAs Move the ast defs wrapper into it's own file 2020-09-28T14:34:06+00:00 Alasdair 2020-09-28T14:01:04+00:00 cf42208a74138a32393073fef574c24bd73a27fc This refactoring is intended to allow this type to have more than just a list of definitions in future. 
This refactoring is intended to allow this type to have more than just a
list of definitions in future.
Fix val_spec to be a better match to user grammar. 2020-09-22T15:07:53+00:00 Mark Wassell 2020-09-22T15:07:53+00:00 9a0d9583ac52abe4b97f6270c86435856eb93d65 






Functorise and refactor C code generator
2020-05-11T18:00:53+00:00

Alasdair

2020-04-28T16:24:04+00:00

199e10df8e776e4b27f9cfd2357db6babf674ed1

Currently uses the -c2 option

Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.

For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.

The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.

Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.





Currently uses the -c2 option

Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.

For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.

The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.

Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.







Allow effects on mappings
2020-01-16T19:14:22+00:00

Alasdair Armstrong

2020-01-16T19:14:22+00:00

bc6b51d70a783df161f8fb43264ea1558ff37bac












Keep track of (non-bit) vectors known to be fixed size in Jib
2020-01-16T14:14:13+00:00

Alasdair Armstrong

2020-01-16T14:11:17+00:00

5c3bf1c0ecaadacdee1888778dde64df99f62e39

This is useful because an arbitrary vector of a fixed size N can be represented symbolically as a
vector of N symbolic values, whereas an arbitrary vector of arbitrary size cannot be easily
represented.





This is useful because an arbitrary vector of a fixed size N can be represented symbolically as a
vector of N symbolic values, whereas an arbitrary vector of arbitrary size cannot be easily
represented.







Basic support to track uncaught exceptions in Sail->C
2020-01-14T21:30:41+00:00

Alasdair

2020-01-14T20:42:37+00:00

057d2b05aa474c27f19dc517f38018414aa91dcf












Don't introduce uneccesary control flow when compiling
2019-12-06T16:42:51+00:00

Alasdair Armstrong

2019-12-06T16:08:08+00:00

d66f510ba6ab9e453c8410fb7a1cab570dd17236












Refactor Jib compilation
2019-11-08T17:22:25+00:00

Alasdair Armstrong

2019-11-08T17:22:25+00:00

bf657ba085f40838a4048b18b19ce889310f3ddd

Split the dynamic context into the ctx struct, and the static
configuration into a module which parameterises the sail->jib
compilation step rather than just having a giant ctx struct.





Split the dynamic context into the ctx struct, and the static
configuration into a module which parameterises the sail->jib
compilation step rather than just having a giant ctx struct.







Backport fixes to SMT generation from poly_mapping branch
2019-11-07T17:48:15+00:00

Alasdair Armstrong

2019-11-07T16:16:14+00:00

51811443eeb7c594b8db9bbffd387dc0fbfeffd3












Fix jib.ott and SMT regressions
2019-10-28T16:30:21+00:00

Alasdair Armstrong

2019-10-28T15:46:40+00:00

da209f9f4bb1772a0b37327fc8d949e240602484

SMT seems sensitive to gensym counter being reset between definitions,
but it shouldn't care due to unique_per_function_ids... need to
investigate further. Only causes a single test to fail so must be
subtle. Diffing between the bad/good versions reveals a few lines of
generated SMT go missing when the gensym counter is reset.





SMT seems sensitive to gensym counter being reset between definitions,
but it shouldn't care due to unique_per_function_ids... need to
investigate further. Only causes a single test to fail so must be
subtle. Diffing between the bad/good versions reveals a few lines of
generated SMT go missing when the gensym counter is reset.