| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |||
| 2018-09-18 | Fix issues with tuple Constructors taking multiple arguments | Alasdair Armstrong | |
| This really demonstrates why we should switch to Typ_fn being a typ list * typ constructor because the implementation here feels *really* hacky with dummy Typ_tup constructors being used to enforce single arguments for constructors. | |||
| 2018-09-18 | Add string mapping functions to interpreter | Alasdair Armstrong | |
| 2018-09-17 | Add diffs to sail files for Aarch64 Coq generation | Brian Campbell | |
| 2018-09-17 | Coq: fix types in aarch64_extras undefined_vector and casts for arguments | Brian Campbell | |
| 2018-09-17 | Coq: solve some constraint/type errors with AArch64 | Brian Campbell | |
| - hints for dotp - handle exists separately when trying eauto to keep search depth low - more uniform existential handling (i.e., we now handle all existentials in the way we used to only handle existentials around atoms) | |||
| 2018-09-17 | Coq: remove an obsolete specialisation | Brian Campbell | |
| Broke E_internal_plet on some simple existential types | |||
| 2018-09-17 | Coq: make generic_neq work on real | Brian Campbell | |
| 2018-09-17 | Rewrites.rewrite_defs_mapping_patterns: emit an explicit type annotation on ↵ | Jon French | |
| the generated pattern so re-typechecking works | |||
| 2018-09-14 | Sail_lib.string_of_bits: print in decimal (properly, with bigints) rather ↵ | Jon French | |
| than binary | |||
| 2018-09-14 | (oops, should have been with "more hex_bits_N monomorphs") | Jon French | |
| 2018-09-14 | Sail_lib.int_of_string_opt: use Big_int.of_string rather than OCaml ↵ | Jon French | |
| int_of_string This fixes e.g. problems with 64-bit bitmask immediates in ARM assembly. | |||
| 2018-09-14 | More monomorphisations for hex_bits_N... | Jon French | |
| I got bored of this so I wrote a Python script to generate all of them between 1 and 33, plus 48 and 64. It's in a comment. We should really get around to making the typechecker work with polymorphic mappings... | |||
| 2018-09-14 | RISCV prelude: fix typo in ocaml extern for negate_* | Jon French | |
| 2018-09-14 | Sail_lib and RISCV prelude: functions for bitwise operations on ints | Jon French | |
| 2018-09-14 | Type_check: allow mappings to contain escape effects | Jon French | |
| 2018-09-13 | C: Fix an issue with assigning to unitialized variables at end of blocks | Alasdair Armstrong | |
| Assigning to an uninitialized variable as the last statement in a block is almost certainly a type, and if that occurs then the lift_assign re-write will introduce empty blocks causing this error to occur. Now when we see such an empty block when converting to A-normal form we turn it into unit, and emit a warning stating that an empty block has been found as well as the probable cause (uninitialized variable). | |||
| 2018-09-13 | Coq: real built-ins for AArch64 | Brian Campbell | |
| 2018-09-12 | Jenkins: Fix deprecation warnings | Alasdair Armstrong | |
| Now that Jenkins is updated to a newer version of OCaml we can finally fix some warning with more recent versions of OCaml than 4.02.3. Also fix a Lem test case that was failing. | |||
| 2018-09-12 | Coq: update RISC-V patch | Brian Campbell | |
| 2018-09-12 | Coq: fix type annotations for early return | Brian Campbell | |
| 2018-09-12 | Coq: make generic_eq work on more types | Brian Campbell | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |