summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-04Bit of commentary, proper TODO errorBrian Campbell
2018-10-03Drop unnecessary thunking; more trouble than it's worthBrian Campbell
2018-10-02Tidy up some whitespaceBrian Campbell
2018-10-02Clean up generator pretty printingBrian Campbell
2018-10-02Remove some old debugging messagesBrian Campbell
2018-10-02Trigger random generator generation with a command line optionBrian Campbell
2018-10-02Rough code to generate random instructions for testingBrian Campbell
(aimed at RISC-V)
2018-09-24Coq: avoid variables called tt (the unit constant)Brian Campbell
2018-09-24Coq: more constraint solutions for aarch64Brian Campbell
2018-09-24Coq: add autocasts at monad returnsBrian Campbell
(This leads to more redundant uses, but I'll tackle that later)
2018-09-21Remove cheri and mips specs -- they now have their own repository.Robert Norton
2018-09-20Tidy up help text for a few optionsBrian Campbell
2018-09-19Coq: track changes elsewhereBrian 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-19Coq: more fixes for AArch64Brian 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-19rewrite_defs_pat_string_append: fix bug with guarded SomeJon French
2018-09-19separate decimal_string_of_bits from string_of_bitsJon French
2018-09-19src/gen_lib/sail2_string.lem: more Lem monomorphisations for ↵Jon French
hex_bits_N_matches_prefix
2018-09-18Fix issues with tuple Constructors taking multiple argumentsAlasdair 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-18Add string mapping functions to interpreterAlasdair Armstrong
2018-09-17Add diffs to sail files for Aarch64 Coq generationBrian Campbell
2018-09-17Coq: fix types in aarch64_extras undefined_vector and casts for argumentsBrian Campbell
2018-09-17Coq: solve some constraint/type errors with AArch64Brian 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-17Coq: remove an obsolete specialisationBrian Campbell
Broke E_internal_plet on some simple existential types
2018-09-17Coq: make generic_neq work on realBrian Campbell
2018-09-17Rewrites.rewrite_defs_mapping_patterns: emit an explicit type annotation on ↵Jon French
the generated pattern so re-typechecking works
2018-09-14Sail_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-14Sail_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-14More 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-14RISCV prelude: fix typo in ocaml extern for negate_*Jon French
2018-09-14Sail_lib and RISCV prelude: functions for bitwise operations on intsJon French
2018-09-14Type_check: allow mappings to contain escape effectsJon French
2018-09-13C: Fix an issue with assigning to unitialized variables at end of blocksAlasdair 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-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Jenkins: Fix deprecation warningsAlasdair 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-12Coq: update RISC-V patchBrian Campbell
2018-09-12Coq: fix type annotations for early returnBrian Campbell
2018-09-12Coq: make generic_eq work on more typesBrian Campbell
2018-09-12Coq: avoid some use of pattern binders to help Coq's type checkerBrian Campbell
2018-09-12Coq: print more type information for existentially typed vectorsBrian Campbell
2018-09-12Coq: remove extra "True"s from constraintsBrian Campbell
The omega tactic doesn't like them
2018-09-11Coq: some basic handling for more existentialsBrian Campbell
2018-09-11Coq: remove a bunch of Lem-ismsBrian Campbell
In particular, the complicated "what nexps are in scope" test can be replaced by a simple "are the nvars in scope" check.
2018-09-11Update coq-riscv snapshot patch and READMEBrian Campbell
2018-09-10RISC-V: move the PC and minstret updates into the step function, to better ↵Prashanth Mundkur
localize them, making loop() purely a platform function.
2018-09-10C: Add documentation for C compilation in manual.texAlasdair Armstrong
2018-09-10Various fixesAlasdair Armstrong
C: Don't print usage message and quit when called with no arguments, as this is used for testing C output OCaml: Fix generation of datatypes with multiple type arguments OCaml: Generate P_cons pattern correctly C: Fix constant propagation to not propagate letbindings with type annotations. This behaviour could cause type errors due to how type variables are introduced. Now we only propagate letbindings when the type of the propagated variable is guaranteed to be the same as the inferred type of the binding. Tests: Add OCaml tests to the C end-to-end tests (which really shouldn't be in test/c/ any more, something like test/compile might be better). Currently some issues with reals there like interpreter. Tests: Rename list.sail -> list_test.sail because ocaml doesn't want to compile files called list.ml.
2018-09-07C: Support RISC-V in elf loader.Prashanth Mundkur
2018-09-07C: add a usage message to the rts.Prashanth Mundkur
2018-09-07Jenkins: Fix Jenkins issue with RISC-V test suiteAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:15:57 +0000