| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Defined in terms of tdiv so we don't have to add it to backends that
don't already have it
|
|
The have_exception flag wasn't being cleared until after the handler,
resulting in false exception reporting.
|
|
Callable as either :f or :step_function
Allow // to be used as a comment in the interactive toplevel
|
|
sail -i now starts an interactive toplevel with a few additional
options set by default:
- It applies the "interpreter" rewrites to any files passed on the command
line.
- It also applies those rewrites after the :l/:load command
- Registers previously started in a disabled state, as the interactive shell
made no default decision as to how to handle undefined (which is the initial
value for all registers). Now -i implies -undefined_gen
- Better help text for :fix_registers
- Nullary interactive actions generate Sail functions that round-trip through pretty
printing and parsing (bugfix)
The -interact_custom flag has the same behavior as the previous -i flag
This commit also improves the c/ocaml/interpreter test harness so it
cleans up temporary files which could cause issues with stale files
when switching ocaml versions
|
|
Allows clients of sail as a library to define custom symbols for $ifdef
and $ifndef
Iterate vector concat assignment and tuple assignment to handle unusual
nesting cases when compiling to C. These rewrites should really be one
rewrite anyway though!
Don't add type annotations when introducing tuple patterns during
rewriting. I guess not adding them could also cause an error in some
circumstances, but if that's the case it could probably be fixed by
tweaking some rules in the type-checker.
|
|
Mention robert's workaround for z3 on WSL
|
|
|
|
|
|
Add documentation for CLion/PyCharm/IntelliJ syntax highlighting
|
|
|
|
From:
No type variable 'ex14#
to:
Type error:
[../and_let_bool.sail]:6:19-50
6 | and_bool(let y : bool = x in not_bool(y), x)
| ^-----------------------------^
| The type variable 'ex14# would leak into an outer scope.
|
| Try adding a type annotation to this expression.
| This error was caused by:
| [../and_let_bool.sail]:6:23-24
| 6 | and_bool(let y : bool = x in not_bool(y), x)
| | ^
| | Type variable 'ex14# was introduced here
|
|
|
Turns out the TextMate Bundles plugin can load the vscode extension and
provide some basic syntax highlighting.
|
|
Allows ASL-to-Sail translation to automatically patch lexp bounds check
errors.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Again use an $ifdef to avoid breaking RMEM. We can't use the same
barrier_kind, because we *really* want a plain enumeration both for
its simple SMT representation and a simple 1 to 1 mapping to the cat
models used by herd.
Technically for Isla, all the read_kind/write_kind/barrier_kind etc
types can be defined separately on a per-architecture basis anyway, so
maybe using this file at all is a bit of an anachronism.
|
|
|
|
Fixes #61
|
|
|
|
|
|
Tells the typechecker that, for example, in a block after
if (i < 0) then {
return ();
} else {
...
}
the constraint not(i < 0) holds. This is a useful pattern when
type-checking code generated from ASL.
|
|
|
|
|
|
Also uncovered a few other issues w.r.t lists
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Allows keeping track of which instructions actually get executed in a trace
|
|
However, use an ifdef to make sure the ifetch changes only appear for the ARM spec, because
otherwise the generated lem for RMEM will break.
|
|
When returning a type from a letbinding we need to be careful that the
type it returns does not refer to any type variable that only exists for
the lifetime of the letbinding (because it was bound by it). Normally
this fails because any type variable bound in the inner letbinding won't
exist in the outer scope, but if it is shadowed this can cause an issue.
|
|
OCaml library
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also be more careful to avoid pattern bindings with identifiers to avoid
parsing clashes, eg `let 'bytes := ...` which is confused with the
notation for binary literals.
|
