| Age | Commit message (Collapse) | Author |
|---|
|
Changes the representation of function types in the ast from
Typ_fn : typ -> typ
to
Typ_fn : typ list -> typ
to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just
multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to
forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...).
In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so
f : (x, y) -> z
f _ = ...
would be disallowed (as _ matches both x and y), forcing
f(_, _) = z
this would simply quite a few things,
Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax
how it is now.
Some issues I noticed when doing this refactoring:
Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function
arguments so maybe it still is.
Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong.
Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same.
|
|
When converting to A-normal form I just used the type of the then
branch of if statements to get the type of the whole if statement -
usually they'd be the same, but with flow typing one of the branches
can have a false constraint, which then allows the optimizer to fit
any integer into a 64-bit integer causing an overflow. The fix is to
correctly use the type the typechecker gives for the whole if
statement.
Also add decimal_string_of_bits to the C output.
Rename is_reftyp to is_ref_typ to be more consistent with other
is_X_typ functions in Ast_util.
|
|
This really demonstrates why we should switch to Typ_fn being a typ
list * typ constructor because the implementation here feels *really*
hacky with dummy Typ_tup constructors being used to enforce single
arguments for constructors.
|
|
|
|
|
|
typing
Added a regression test as c/test/downcast_fn.sail
|
|
|
|
constructors
Add a new printing function for debugging that recursively prints
constructor types.
Fix an interpreter bug when pattern matching on constructors with
tuple types.
|
|
Now all we need to do is make sure the RISC-V builtins are mapped to
the correct C functions, and RISC-V in C should work
(hopefully). We're still missing some of the functions in sail.c for
the mappings so those have to be implemented.
|
|
Allow pat_lits rewrite to map L_unit to wildcard patterns, rather than
introducing eq_unit tests as guards.
Add a fold_function and fold_funcl functions in rewriter.ml that apply
the pattern and expression algebras to top-level functions, which
means that they correctly get applied to top-level function patterns
when they are used. Currently modifying the re-writing passes to do
this introduces some bugs which needs investigated further. The
current situation is that top-level patterns and patterns elsewhere
are often treated differently because rewrite_exp doesn't (and indeed
cannot, due to how the re-writer is structured) rewrite top level
patterns.
Fix pattern completeness check for unit literals
Fix a bug in Sail->ANF transform where blocks were always annotated
with type unit incorrectly. This caused issues in pattern literal
re-writes where the guard was a block returning a boolean. A test case
for this is added as test/c/and_block.sail.
Fix a bug caused by nested polymorphic function calls and matching in
top-level patterns. Test case is test/c/tl_poly_match.sail.
Pass location info through codegen_conversion for better error
reporting
|
|
This change allows the RISC-V spec to compile to C, but more testing
is needed to ensure it works correctly.
|
|
Make the C l-expression type in Sail more generic and expressive, and
refactor the generation of conversions into a seperate
codegen_conversion function, which can handle more complex cases than
the previous more ad-hoc method.
|
|
Ensure that this works even when the union types are dependent in the wrong order, before topologically sorting definitions. We do this by calling fix_variant_ctyps on all cdefs by passing a list of
prior cdefs to specialize_variants.
|
|
Test the builtin functions by compiling them to C, OCaml, and OCaml
via Lem. Split up some of the longer builtin test programs to avoid
stack overflows when compiling to OCaml, as 3000+ line long blocks can
cause issues with some re-writing steps.
Also test constant-folding with builtins (this should reduce the
asserts in these files to assert true), and also test constant folding
with the C compilation.
Fix a bug whereby vectors with heap-allocated elements were not
initialized correctly.
Fix a bug caused by compiling and optimising empty vector literals.
Fix an OCaml test case that broke due to the ref type being used. Now
uses references to registers.
Fix a bug where Sail would output big integers that lem can't
parse. Checks if integer is between Int32.min_int and Int32.max_int
and if not, use integerOfString to represent the integer. Really this
should be fixed in Lem.
Make the python test runner script the default for testing builtins
and running the C compilation tests in test/run_tests.sh
Add a ocaml_build_dir option that sets a custom build directory for
OCaml. This is needed for running OCaml tests in parallel so the
builds don't clobber one another.
|
|
|
|
Add additional well-formedness check when calling typing rules
|
|
|
|
Cleanup some debugging output
|
|
|
|
We now generate anonymous types in the correct order, but post specialisation more dependencies can occur between named types, so an additional
sorting step is needed to ensure that these happen in the correct order. In theory we could end up with circular dependencies here that don't exist
at the Sail source level, but this shouldn't occur often (or ever) in practice. I think this is fixable but it would require some code generator
changes.
|
|
lifted types
Add a test case for nested variant constructors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
types
|
|
|
|
Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging
|
|
|
|
|
|
By default generated functions are non-static, using the -static flag makes them static which is useful for measuring coverage using generated code. Some utility helper functions will always be static, but the compiled versions of sail functions won't be unless this flag is set.
|
|
Makes sure equality comparisons for variants are compiled correctly. Needed for CHERI and mips, which have structs containing
variants. Also make sure that struct equality works for structs containing other structs.
|
|
Add a test case in test/c/eq_struct.sail. Ensure that the macro EQUAL(type) will always give a valid equality function for any
builtin type in sail.h.
|
|
|
|
Non bitvector literals for decreasing vectors were not being reversed
correctly, so the list of capability registers was effectively in
reverse order.
Added a test case to test/c/ based on this aspect of CHERI
|
|
to notice if they are dead or inline them if appropriate, cleaning up coverage reports and potentially improving execution speed.
|
|
We should test before the first iteration in case 'to' starts out as
less than 'from'.
|
|
The code to do this is rather ugly. It would be nice to have a generic
callgraph representation we could just query and not use the rewriter
in a weird way to extract this info.
|
|
|
|
|
|
|
|
This is now directly supported from SAIL so we can call the SAIL __SetConfig function
instead.
|
|
Registers can now be marked as configuration registers, for example:
register configuration CFG_RVBAR = 0x1300000
They work like ordinary registers except they can only be set by
functions with the 'configuration' effect and have no effect when
read. They also have an initialiser, like a let-binding. Internally
there is a new reg_dec constructor DEC_config. They are intended to
represent configuration parameters for the model, which can change
between runs, but don't change during execution. Currently they'll
only work when compiled to C. Internally registers can now have custom
effects for reads and writes rather than just rreg and wreg, so the
type signatures of Env.add_register and Env.get_register have changed,
as well as the Register lvar, so in the type checker we now write:
Env.add_register id read_effect write_effect typ
rather than
Env.add_register id typ
For the corresponding change to ASL parser there's a function
is_config in asl_to_sail.ml which controls what becomes a
configuration register for ARM. Some things we have to keep as
let-bindings because Sail can't handle them changing at runtime -
e.g. the length of vectors in other top-level definitions. Luckily
__SetConfig doesn't (yet) try to change those options.
Together these changes allow us to translate the ASL __SetConfig
function, which means we should get command-line option compatibility
with ArchEx for running the ARM conformance tests.
|
|
Also further tweaks to Sail library for C and include sail lib files for tracing
|
|
Refactor the C compilation process by moving out the conversion to
A-normal form into its own file. Also make the A-normal form AST
parameterised by the type of the types annotating it. The idea being we
can have a typ aexp -> ctyp aexp translation, converting to low-level
types at a slightly higher level before mapping into our low-level IR.
This would fix some issues we have where the type of variables change
due to flow typing, because we could map the sail types to low-level
types in the ANF ast where we still have some knowledge about the
structure of the original Sail.
|
