summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-29Output a few more type annotations for LemThomas Bauereiss
Allow pretty-printing of existential types, if the existentially quantified variables do not actually appear in the Lem output. This is useful for the bit list representation of bitvectors, as it will print the type annotation "list bitU" for bitvectors whose length depends on an existentially quantified variable.
2018-01-29Add a fixme for unhandled fences but allow them to execute.Prashanth Mundkur
2018-01-29Initial handling of CSR reads/writes.Prashanth Mundkur
2018-01-29Add satp to CSR dummy implemented predicate. Also direct the illegal ↵Prashanth Mundkur
instruction exception through the exception handler.
2018-01-29use check target in makefile when checking riscv spec.Robert Norton
2018-01-29riscv: fix warnings about incomplete patterns. Add a check target in ↵Robert Norton
Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings.
2018-01-29Sync mono rewrites definitions with libraryBrian Campbell
2018-01-29Look through let expressions when constructing nconstraintsBrian Campbell
(needed for handling guards after atom-to-itself transformation in monomorphisation)
2018-01-29Leave pure if-conditions in place instead of pulling out let-bindingsBrian Campbell
2018-01-29Set maximum split size to work with aarch64 no vectorBrian Campbell
2018-01-29Get typechecking to resolve overriding in remove numeral patterns rewriteBrian Campbell
2018-01-29Move subst to ast_util, use for guarded clauses rewriteBrian Campbell
2018-01-29Add some initial exception handling to the riscv execution loop.Prashanth Mundkur
2018-01-29Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Robert Norton
2018-01-29riscv: remove break from main loop and place val spec in prelude.Robert Norton
2018-01-29riscv: add tracing of register writes.Robert Norton
2018-01-29add tohost to value.mlRobert Norton
2018-01-29implement shift primitives in sail_lib.mlRobert Norton
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-29Fix error in RISCV: SLLI and SRLI were swapped...Robert Norton
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 11:22:02 +0000