| Age | Commit message (Collapse) | Author |
|---|
|
Fix a bug where we generated empty definitions which pre 4.07 versions
of OCaml don't appear to support.
|
|
|
|
|
|
We want to ensure that no_devices.sail and devices.sail have the same
effect footprint, because with a snapshot-type release in sail-arm, we
can't rebuild the spec with asl_to_sail every time we switch from
running elf binaries to booting OS's. This commit allows registers to
have arbitrary effects, so registers that are really representing
memory-mapped devices don't have to have the wmem/rmem effect.
|
|
Remove unused name schemes and DEF_kind
|
|
|
|
Some of the output from the tests scripts is odd on Jenkins, try to
fix this by flushing stdout more regularly in the test scripts
|
|
Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of
uvar as the result of unify. Plus A_ could either stand for argument, or
Any/A type which is quite appropriate in most use cases.
Restore instantiation info in infer_funapp'. Ideally we would save this
instead of recomputing it ever time we need it. However I checked and
there are over 300 places in the code that would need to be changed to add
an extra argument to E_app. Still some issues causing specialisation to
fail however.
Improve the error message when we swap how we infer/check an l-expression,
as this could previously cause the actual cause of a type-checking failure
to be effectively hidden.
|
|
On a new branch because it's completely broken everything for now
|
|
This makes dealing with records and field expressions in Sail much
nicer because the constructors are no longer stacked together like
matryoshka dolls with unnecessary layers. Previously to get the fields
of a record it would be either
E_aux (E_record (FES_aux (FES_Fexps (fexps, _), _)), _)
but now it is simply:
E_aux (E_record fexps, _)
|
|
|
|
|
|
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)
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(aimed at RISC-V)
|
|
Now that Jenkins is updated to a newer version of OCaml we can finally
fix some warning with more recent versions of OCaml than 4.02.3. Also
fix a Lem test case that was failing.
|
|
C: Don't print usage message and quit when called with no arguments,
as this is used for testing C output
OCaml: Fix generation of datatypes with multiple type arguments
OCaml: Generate P_cons pattern correctly
C: Fix constant propagation to not propagate letbindings with type
annotations. This behaviour could cause type errors due to how type
variables are introduced. Now we only propagate letbindings when the
type of the propagated variable is guaranteed to be the same as the
inferred type of the binding.
Tests: Add OCaml tests to the C end-to-end tests (which really
shouldn't be in test/c/ any more, something like test/compile might be
better). Currently some issues with reals there like interpreter.
Tests: Rename list.sail -> list_test.sail because ocaml doesn't want
to compile files called list.ml.
|
|
|
|
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.
|
|
|
|
One day we will be free from the 4.02.3 menace, but today is not that day. :(
This should fix Sail on Jenkins
This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414.
|
|
Changes are:
- String.capitalize -> String.capitalize_ascii
- String.uppercase -> String.uppercase_ascii
- String.lowercase -> String.lowercase_ascii
Basically just making the change that the warning message suggested.
|
|
|
|
targets using this.
|
|
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.
|
|
Big_int literals.
Improves tests/riscv duration by around 2% and size of riscv.o by 15%.
|
|
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).
|
|
|
|
|
|
default (off by default).
|
|
version instead and make sure to install util and copy it to ocaml build directory.
|
|
builds this defaults to git root.
|
|
files in installed location.
|
|
Fixes #11
|
|
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 for loop in interactive interpreter
Fixes #8
|
|
One caveat still: Won't work if the polymorphic definition consists of
multiple function clauses, but this seems unlikely - and I added an
error message if this is the case.
Also fix a small flow typing bug
Fixes #7
|
|
Fixes #6
|
|
Added a regression test in test/ocaml/string_of_struct
|
|
|
|
Also updated some of the documentation in the sail source code
|
|
|
