| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-23 | RISC-V: implement terminal output for C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: tick the clock in the C platform. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Add device tree blob into rom, currently only when linked against spike. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: add default reset vector. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: fix up platform bits for lr/sc. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: set htif tohost port address using ELF symbol. | Prashanth Mundkur | |
| 2018-10-23 | RTS: Add elf symbol lookup support. | Prashanth Mundkur | |
| 2018-10-23 | Fix typo in plat_ram_size | Alasdair Armstrong | |
| 2018-10-23 | RISC-V: Add some debug logs for within_phys_mem. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Allow Spike linkage to be conditionally enabled. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: flush logs at each step. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Flesh out more of the tandem checks in the C platform simulator. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: An initial C Sail model linked against Spike for testing. | Prashanth Mundkur | |
| 2018-10-23 | RTS: allow elf-loader to provide entry info. | Prashanth Mundkur | |
| 2018-10-23 | RISC-V: Refactor c platform bits. | Prashanth Mundkur | |
| 2018-10-22 | Coq: use function type more carefully in untupling | Brian Campbell | |
| And update the RISC-V patch accordingly. | |||
| 2018-10-22 | Update Coq patch for RISC-V, add string_take to Coq library | Brian Campbell | |
| 2018-10-22 | Coq: work around constructors with tupled arguments | Brian Campbell | |
| 2018-10-22 | Fix lem arguments for functions with tuple arguments | Alasdair Armstrong | |
| Make lem output understand difference between functions taking a tuple and functions taking multiple arguments. Previously it assumed that no functions ever took a tuple as an argument, which is incorrect for mappings. | |||
| 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 | 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-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 | 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 | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |