| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We need to ensure that we expand type-synonyms when calculating which
types a register depends on during topological sorting in order to
place the undefined_type function in the correct place, even when type
is indirected through a function.
|
|
When topologically sorting the top-level definitions, we add the
undefined_X functions for any type X to a registers dependencies if it
uses the type X, this ensures that any such functions are generated
before the register declaration. In theory this is only needed for
OCaml, but adding these edges in the definition graph shouldn't cause
any issues.
|
|
For ASL parser, we have code that can add additional constraints to a
function if they are required by functions it calls, but for more
general range analysis we need to restrict the return types of various
ASL functions that return int. To do this we can write some code that
walks over the type-checked AST for a function body and tries to infer
a more restrictive return type at each function exit point. Then we
try to union those types together if possible to infer a more
restricted return type.
For example, for the highest_set_bit function
val highest_set_bit : forall ('n : Int), 'n >= 0. bits('n) -> int
function highest_set_bit x = {
foreach (i from ('n - 1) to 0 by 1 in dec) {
print_int("idx = ", i);
if [x[i]] == 0b1 then return(i) else ()
};
return(negate(1))
}
Which is annotated as returning any int, we can synthesise a return
type of
{'m, ('m = -1 | (0 <= 'm & 'm <= ('n - 1))). int('m)}
Currently I have this code in Sail as it's likely also useful as a
optimisation/lint but it could also live in the asl_parser repository.
|
|
(only affects Reduce on Aarch64)
|
|
Also some pretty printer improvements
Make all the tests use the same colours for green/red/yellow
|
|
Doesn't work with nested not-patterns, but I think we should probably
just disallow these as they seem very hard to remove in any kind of
sensible way.
|
|
Remove Parse_ast.Int (for internal locations) as this was unused. Add
a Parse_ast.Unique constructor to create unique locations. Change
locate_X functions to take a function modifying locations, rather than
just replacing them and add a function unique : l -> l that makes
locations unique, such that `locate unique X` will make a locations in
X unique.
|
|
There is no Reporting_complex, so it's not clear what the basic is
intended to signify anyway.
Add a GitHub issue link to any err_unreachable errors (as they are all
bugs)
|
|
For example, for a function like
```
val aget_X : forall 'n, 0 <= 'n <= 31. int('n) -> bits(64)
function test(n : int) -> unit = {
let y = aget_X(n);
()
}
```
we get the message
> Could not resolve quantifiers for aget_X (0 <= 'ex7# & 'ex7# <= 31)
>
> Try adding named type variables for n : atom('ex7#)
>
> The property (0 <= n & n <= 31) must hold
which suggests adding a name for the type variable 'ex7#, and gives
the property in terms of the variable n. If we give n a type variable name:
```
val test : int -> unit
function test(n as 'N) = {
let y = aget_X(n);
()
}
```
It will suggest a constraint involving the type variable name
> Could not resolve quantifiers for aget_X (0 <= 'ex6# & 'ex6# <= 31)
>
> Try adding the constraint (0 <= 'N & 'N <= 31)
|
|
No longer remove braces around singleton expressions, as this can
produce unreadably long lines in ASL parser output when assignments
are converted to lets.
Add brackets around as-patterns for type-variables
|
|
Merge C platform bits for RISC-V
|
|
Currently not enabled by default, the flag -Xconstraint_synonyms
enables them
For generating constraints in ASL parser, we want to be able to give
names to the constraints that we attach to certain variables. It's
slightly awkward right now when constraints get long complicated
because the entire constraint always has to be typed out in full
whenever it appears, and there's no way to abstract away from that.
This adds constraint synonyms, which work much like type synonyms
except for constraints, e.g.
constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256
these constraints can then be used instead of the full constraint, e.g.
val f : forall 'n, where Size('n). int('n) -> unit
Unfortunatly we need to have a keyword to 'call' the constraint
synonym otherwise the grammer stops being LR(1). This could be
resolved by parsing all constraints into Parse_ast.atyp and then
de-sugaring them into constraints, which is what happens for
n-expressions already, but that would require quite a bit of work on
the parser.
To avoid this forcing changes to any other parts of Sail, the intended
invariant is that all constraints appearing anywhere in a type-checked
AST have no constraint synonyms, so they don't have to worry about
matching on NC_app, or calling Env.expand_typquant_synonyms (which
isn't even exported for this reason).
|
|
|
|
Also add a brief README for booting Linux on the C and OCaml backends.
|
|
|
|
|
|
possible without linking to Spike.
When linked with Spike, ensure that the DTBs being used are identical.
|
|
|
|
faults.
|
|
- add mstatus to cross-check
- fix typo in assembly mapping for lr/sc
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
And update the RISC-V patch accordingly.
|
|
|
|
|
|
Make lem output understand difference between functions taking a tuple
and functions taking multiple arguments. Previously it assumed that no
functions ever took a tuple as an argument, which is incorrect for
mappings.
|
|
actually take a tuple argument
|
|
|
|
Uses new primop 'string_take' which is much easier to implement in e.g. C
|
|
rewrite_defs_pat_lits
|
|
|
|
that this information propagates from the instruction definition to
the memory accesses. Necessary for Promising RISC-V concurrency model.
|
|
|
|
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.
|
