summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell
2018-06-18Separate bitvector access/update from generic vector access in std preludeBrian Campbell
(necessary for backends where they're different) Coq uint/sint and related fixes
2018-06-18Coq: fix up some comparison operations in preludeBrian Campbell
2018-06-18Coq: update prompt monad wrt LemBrian Campbell
2018-06-13Coq: library updates, informative type errors, fix type aliasesBrian Campbell
(The last bit is to declare type aliases as Type so that Coq uses the type scope for notation, so * is prod, not multiplication).
2018-06-12Coq: support for range type, along with related existential improvementsBrian Campbell
Plus - Complete solver support for inequalities - Reduce exponentials in solver
2018-06-12Coq: add more to libraryBrian Campbell
2018-06-11actually fix exist_pattern testJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-06-11Add string.sail file to libAlasdair Armstrong
2018-06-11Merge branch 'sail2' into mappingsJon French
(involved some manual tinkering with gitignore, type_check, riscv)
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
Plus test case, broken builtin name
2018-06-08Coq: existential and constraint solving workBrian Campbell
- add existential unpacking for function arguments - add mechanism for using properties for existentially typed top-level values (useful for the typechecking tests) - support for length_list and In in Coq constraint solving
2018-06-08Coq: some very basic existential supportBrian Campbell
Only single variable in places, only packed at literals and variables, no unpacking
2018-06-08Fill in most Coq built-insBrian Campbell
2018-06-08Add missing Coq builtin info to vector_incBrian Campbell
2018-06-07Fix bug in add_bits optimizationAlasdair Armstrong
2018-06-07Rename some functions in vector_dec library file to avoid clashes with ↵Robert Norton
functions in mips spec in prepartion for using this file in mips prelude. Also modify tests that use this header. We should consider prefixing library builtins to avoid name clashes. overload can then be used to provide aliases if desired.
2018-06-07Fixes and additions to c builtins needed to pass mips test suite. bv_ts ↵Robert Norton
should be kept in normal form i.e. a positive mpz_t with no bits higher than len set.
2018-06-04Update sail C libraryAlasdair Armstrong
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
Also fixes to C backend for compiling MIPS spec to C - Fix an issue with const correctness in internal_vector_update functions generated by C backend - Add builtins for MIPS to sail.h - Fix an issue where reg_deref didn't work when called on pointers to large bitvectors, i.e. vectors containing references to large bitfields as in the MIPS TLB code - Various bug fixes and changes for running U-boot on ARM model, including for interpreter and OCaml compilation. - Fix memory leak issues and incorrect shadowing for foreach loops - Update C header file. Fixes memory leak in memory read/write builtins. - Add aux constructor to ANF representation to hold environment information. - Fix undefined behavior caused by optimisation left shifting uint64_t vectors 64 or more times. Unfortunately there's more issues because the same happens for X >> 64 right shifts. It would make sense for this to be zero, because that would guarantee the property that ((X >> n) >> m) == (X >> (n + m)) but we probably need to do (X >> (n - 1) >> 1) in the optimisation to ensure that we don't cause UB. Shifting by 63 and then by 1 is well-defined, but shifting by 64 in one go isn't according to the C standard. This issue with right-shifts only occurs for zero-length vectors, so it's not a huge deal, but it's still annoying. - Add versions of print_bits and print_int that print to stderr. Follows OCaml convention of print/prerr. Should make things more explicit. Different backends had different ideas about where print should output to, not every backend needs to have this (e.g. theorem prover backends don't need to print) but having both stderr and stdout seperate and clear is useful for executable models (UART needs to be stdout, debug messages should be stderr).
2018-05-31Add auxiliary script to HolmakefileRamana Kumar
2018-05-31Add some HOL4 termination proofs for state.lemRamana Kumar
2018-05-25Coq: fill in some built-insBrian Campbell
vector_access is a bit hacky at the moment - it expects a constraint to be shown between the index and the list size, but we don't track list sizes in general
2018-05-25allow loading multiple raw files in ocaml main backend to allow kernel and ↵Robert Norton
dtb to be mapped.
2018-05-24Coq: solve more constraintsBrian Campbell
2018-05-24Help launch coqideBrian Campbell
2018-05-24Import (rather hacky) Coq Sail librariesBrian Campbell
2018-05-23A couple of missing >= 0 constraints on vector handling functionsBrian Campbell
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-18Add lemmas about monadic Boolean connectivesThomas Bauereiss
2018-05-18use correct inequality for strings.Robert Norton
2018-05-18Add sail_valuesAuxiliary rw theorems to computeLibRamana Kumar
2018-05-18Improve sail-heap dependencies in the HolmakefileRamana Kumar
2018-05-18Avoid split_on_char function that was introduced in OCaml 4.04. Use Util ↵Robert Norton
version instead and make sure to install util and copy it to ocaml build directory.
2018-05-17changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ↵Robert Norton
ocaml main so that we can have simboot + kernel. Support UART output only.
2018-05-17Merge branch 'cheri-mono' into sail2Brian Campbell
2018-05-17Clean up MIPS for HOL4 a littleBrian Campbell
Move mono_rewrites into lib
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
resolving the difference in type parameters between the prompt and state monads, and allowing a single output file to be used with either. Normally, the type alias is to the prompt monad, but for HOL4 we use the state monad.
2018-05-16Add handwritten script to HolmakefileBrian Campbell
2018-05-16More targeted gitignore for HOL4Brian Campbell
(will do individual models later)
2018-05-16Termination proofs and lemmata for sail_values holRamana Kumar
2018-05-15Merge branch 'sail2' into mappingsJon French
2018-05-15Make all of Sail HOL libraries, not just the base heapBrian Campbell
2018-05-11Add snapshot of generated Isabelle theoriesThomas Bauereiss
Currently contains Lem and Sail libraries, and RISC-V and CHERI-MIPS specs.
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
In order to use up-to-date sequential CHERI model for test suite
2018-05-10RISC-V in HOL4Brian Campbell
2018-05-10Clean up HOL library properlyBrian Campbell
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-09Fix an issue with C compilationAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 10:03:39 +0000