summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-29Further updates to C backendAlasdair Armstrong
2018-01-29Added ecall/mret and exception support.Prashanth Mundkur
2018-01-29Fix a bug where structs containing unions would generate bad to_string functionsAlasdair Armstrong
Added a regression test in test/ocaml/string_of_struct
2018-01-29Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-29Shaked removing generation of now-uncessary uint dependencyPeter Sewell
2018-01-29Linksem does not use uint anymoreShaked Flur
2018-01-29Turn off constraint substitution in monoBrian Campbell
(Type checker doesn't seem to use false aggressively enough for this)
2018-01-29Use fresh variables when dealing with (multiple) literal patternsBrian Campbell
2018-01-29Turn off warnings when rechecking after monoBrian Campbell
2018-01-29Avoid generating (_ as n) in mono, broke atom type rewritingBrian Campbell
2018-01-27Add Makefile for RISC-VThomas Bauereiss
2018-01-26Fixed loading ARM elf filesAlasdair Armstrong
Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib
2018-01-26One more mono rewriteBrian Campbell
2018-01-26Missing -ocamlfindBrian Campbell
2018-01-26Add replacement of complex nexp sizes by equivalent variables in monoBrian Campbell
2018-01-26Preserve more typing info in monomorphisation for later stagesBrian Campbell
2018-01-26More work on C backendAlasdair Armstrong
2018-01-26Give LEM test suite a more useful name for benefit of jenkins.Robert Norton
2018-01-26Shebang must be first line of file. Fixes RISCV test failing on jenkins due ↵Robert Norton
to non-bash default shell.
2018-01-25Add mli file for pattern completeness moduleAlasdair Armstrong
2018-01-25Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-25Add pattern completness check for match statementsAlasdair Armstrong
Gives warnings when pattern matches are incomplete, when matches are redundant (in certain cases), or when no unguarded patterns exist. For example the following file: enum Test = {A, C, D} val test1 : Test -> string function test1 x = match x { A => "match A", B => "this will match anything, because B is unbound!", C => "match C", D => "match D" } val test2 : Test -> string function test2 x = match x { A => "match A", C => "match C" /* No match for D */ } val test3 : Test -> string function test3 x = match x { A if false => "never match A", C => "match C", D => "match D" } val test4 : Test -> string function test4 x = match x { A if true => "match A", C if true => "match C", D if true => "match D" } will produce the following warnings Warning: Possible redundant pattern match at file "test.sail", line 10, character 5 to line 10, character 5 C => "match C", Warning: Possible redundant pattern match at file "test.sail", line 11, character 5 to line 11, character 5 D => "match D" Warning: Possible incomplete pattern match at file "test.sail", line 17, character 3 to line 17, character 7 match x { Most general matched pattern is A_|C_ Warning: Possible incomplete pattern match at file "test.sail", line 26, character 3 to line 26, character 7 match x { Most general matched pattern is C_|D_ Warning: No non-guarded patterns at file "test.sail", line 35, character 3 to line 35, character 7 match x { warnings can be turned of with the -no_warn flag.
2018-01-25Use set asserts as case splits in monomorphisationBrian Campbell
2018-01-25Missing type expansionBrian Campbell
2018-01-25Handle bound variables properly with precise case splittingBrian Campbell
2018-01-25Fix building bytecode sailBrian Campbell
2018-01-25Basic support for match x[5 .. 2] with case splitsBrian Campbell
2018-01-25Implement basic case splitting based on found case expressionsBrian Campbell
(makes some of the monomorphisation case splits smaller)
2018-01-25Extend RISCV main loop with support for tohost interface used by test suite ↵Robert Norton
for terminating the test.
2018-01-25Omit redundant let-bindings when rewriting (bit-)vector patternsThomas Bauereiss
Only add bindings for sub-patterns if they are actually used in the pattern guard or expression, respectively.
2018-01-25Rewrite bitvector patterns for OCaml and C backendsThomas Bauereiss
Seems to increase compilation speed significantly for OCaml 4.05.
2018-01-25Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-25Fix -ocaml_trace optionAlasdair Armstrong
2018-01-25riscv: remove case for non-existent constructor in match that was being ↵Robert Norton
treated as pattern making _ never match :-(
2018-01-25work in progress riscv CSR implementation.Robert Norton
2018-01-25Fix more type annotations in rewriterThomas Bauereiss
Use consistent nesting of tuples when adding updated local mutable variables to expressions. Add test case.
2018-01-25Add simple conditional processing and file includeAlasdair Armstrong
Can now use C-style include declarations to include files within other sail files. This is done in such a way that all the location information is preserved in error messages. As an example: $include "aarch64/prelude.sail" $define SYM $ifndef SYM $include <../util.sail> $endif would include the file aarch64/prelude.sail relative to the file where the include is contained. It then defines a symbol SYM and includes another file if it is not defined. The <../util.sail> include will be accessed relative to $SAIL_DIR/lib, so $SAIL_DIR/lib/../util.sail in this case. This can be used with the standard C trick of $ifndef ONCE $define ONCE val f : unit -> unit $endif so no matter how many sail files include the above file, the valspec for f will only appear once. Currently we just have $include, $define, $ifdef and $ifndef (with $else and $endif). We're using $ rather than # because # is already used in internal identifiers, although this could be switched.
2018-01-24Have some simple sail programs compiling to CAlasdair Armstrong
2018-01-24Fixed riscv ocaml compilationAlasdair Armstrong
2018-01-24More work on C compilationAlasdair Armstrong
2018-01-24More work on experimental C backendAlasdair Armstrong
2018-01-23Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-23Started working on C backend for sailAlasdair Armstrong
Also updated some of the documentation in the sail source code
2018-01-23Run tests for Lem shallow embeddingThomas Bauereiss
Uses the typechecker tests for now. Also fix two minor bugs in pretty-printer and rewriter uncovered by the tests.
2018-01-23Added additional tests, and fixed ocaml build of ARM testsAlasdair Armstrong
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.
2018-01-22Added rewriter that specializes all function calls in a specification.Alasdair Armstrong
This removes all type polymorphism, so we can generate optimized bitvector code and compile to languages without parametric polymorphism.
2018-01-22Add regression test for type synonym with constraints inside existential ↵Alasdair Armstrong
typechecking bug
2018-01-22Update and fix test suiteAlasdair Armstrong
2018-01-19Added RISCV test case to test suiteAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 17:57:19 +0000