| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-24 | add a couple things to gitignore | Jon French | |
| 2018-10-24 | Interpreter: add handling of undefs and sizeofs, and initialize registers to ↵ | Jon French | |
| undefined on startup | |||
| 2018-10-24 | Interpreter: improve error handling/messages | Jon French | |
| 2018-10-24 | src/Makefile: add isail.byte target for debugging interpreter | Jon French | |
| 2018-10-24 | Interpreter: don't silently use OCaml externs, only interpreter externs | Jon French | |
| (Adds 'interpreter' externs as appropriate.) | |||
| 2018-10-22 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-10-22 | Pretty_print_lem.untuple_args_pat: temporary hack to allow functions that ↵ | Jon French | |
| actually take a tuple argument | |||
| 2018-10-16 | Merge branch 'sail2' into rmem_interpreter | Jon French | |
| 2018-10-16 | add a couple more RISC-V things to gitignore | Jon French | |
| 2018-10-16 | Re-implement space-related mapping functions in Sail rather than backends | Jon French | |
| Uses new primop 'string_take' which is much easier to implement in e.g. C | |||
| 2018-10-16 | rewrites: remove now-unnecessary temporary string hack from ↵ | Jon French | |
| rewrite_defs_pat_lits | |||
| 2018-10-15 | Update manual snapshot | Alasdair Armstrong | |
| 2018-10-15 | Ocaml backend: omit function definitions for externs | Jon French | |
| 2018-10-15 | Add interpreted RISC-V model to test suite | Jon French | |
| 2018-10-15 | Interpreter: add new command :bin <addr> <file> to load raw binary into memory | Jon French | |
| 2018-10-13 | Adapt checked_mem_read to have acquire/release/reserve arguments so | Christopher Pulte | |
| that this information propagates from the instruction definition to the memory accesses. Necessary for Promising RISC-V concurrency model. | |||
| 2018-10-12 | Prevent accidental test failures when Coq compiles in the wrong order | Brian Campbell | |
| 2018-10-11 | Change the function type in the AST | Alasdair | |
| 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. | |||
| 2018-10-10 | refer to Util.list_init.ml rather than List.init in sail_lib.ml | Christopher Pulte | |
| 2018-10-08 | Interpreter: refactor get/put state into more fine-grained responses in the ↵ | Jon French | |
| monad | |||
| 2018-10-08 | Produce lists of constructors and ast building functions for test generation | Brian Campbell | |
| 2018-10-05 | interpreter: Remove boxes (no longer used) | Jon French | |
| 2018-10-05 | RISC-V: encode/decode and assembly mappings for compressed instructions | Jon French | |
| 2018-10-05 | fix bug in infer_mpat losing types of identifiers inferred from other_env | Jon French | |
| 2018-10-04 | Merge branch 'ocaml-instruction-generation' into sail2 | Brian Campbell | |
| 2018-10-04 | Bit of commentary, proper TODO error | Brian Campbell | |
| 2018-10-04 | rename stringappend ids for more readable generated code | Jon French | |
| 2018-10-03 | Drop unnecessary thunking; more trouble than it's worth | Brian Campbell | |
| 2018-10-02 | Tidy up some whitespace | Brian Campbell | |
| 2018-10-02 | Clean up generator pretty printing | Brian Campbell | |
| 2018-10-02 | Remove some old debugging messages | Brian Campbell | |
| 2018-10-02 | Trigger random generator generation with a command line option | Brian Campbell | |
| 2018-10-02 | Rough code to generate random instructions for testing | Brian Campbell | |
| (aimed at RISC-V) | |||
| 2018-10-01 | Update Coq RISC-V patch now that the assembler is in good shape | Brian Campbell | |
| 2018-10-01 | Extend Coq pattern match completeness rewrite to let patterns | Brian Campbell | |
| 2018-10-01 | New rewriting pass toplevel_string_append | Jon French | |
| Handles the common case of a single level string append pattern in a way designed to be friendlier to Coq etc, by generating an auxiliary function for each pattern rather than emitting a massive nested pattern match twice. | |||
| 2018-09-28 | Add a regression test for bug in commit 88b25e9 | Alasdair Armstrong | |
| 2018-09-28 | Fix optimisation bug for certain if statements | Alasdair Armstrong | |
| When converting to A-normal form I just used the type of the then branch of if statements to get the type of the whole if statement - usually they'd be the same, but with flow typing one of the branches can have a false constraint, which then allows the optimizer to fit any integer into a 64-bit integer causing an overflow. The fix is to correctly use the type the typechecker gives for the whole if statement. Also add decimal_string_of_bits to the C output. Rename is_reftyp to is_ref_typ to be more consistent with other is_X_typ functions in Ast_util. | |||
| 2018-09-27 | Add new functions in ast_util.ml for working with locations | Alasdair Armstrong | |
| When constructing expressions, we need to provide locations for the generated expressions to give useful error messages. However adding these at every mk_X function in ast_util would be very verbose, especially for complex expressions. Add new locate_X functions (with the one for expressions simply being called locate), which take a location and recursively apply it to every child node, e.g. locate (gen_loc l) (mk_exp (... (mk_exp ..., mk_exp ...))) would mark every part of the constructed expression as being generated from code at location l. | |||
| 2018-09-27 | Add an additional type checking test | Alasdair Armstrong | |
| 2018-09-24 | Coq: avoid variables called tt (the unit constant) | Brian Campbell | |
| 2018-09-24 | Coq: more constraint solutions for aarch64 | Brian Campbell | |
| 2018-09-24 | Coq: add autocasts at monad returns | Brian Campbell | |
| (This leads to more redundant uses, but I'll tackle that later) | |||
| 2018-09-21 | Remove cheri and mips specs -- they now have their own repository. | Robert Norton | |
| 2018-09-20 | Tidy up help text for a few options | Brian Campbell | |
| 2018-09-19 | Coq: track changes elsewhere | Brian Campbell | |
| - more hex_bits functions, add decimal_string_of_bits - extra tuple unfolding in constructors - note that variables can be redundant wildcard clauses - update RISC-V patch | |||
| 2018-09-19 | Coq: more fixes for AArch64 | Brian Campbell | |
| - implement set_slice and set_slice_int - lemmas for more constraints - make real sqrt visible - unfolding list membership needs andb and orb to be handled first | |||
| 2018-09-19 | rewrite_defs_pat_string_append: fix bug with guarded Some | Jon French | |
| 2018-09-19 | separate decimal_string_of_bits from string_of_bits | Jon French | |
| 2018-09-19 | src/gen_lib/sail2_string.lem: more Lem monomorphisations for ↵ | Jon French | |
| hex_bits_N_matches_prefix | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |