summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Collapse)Author
2018-06-27RTS: Add support for __ListConfigAlastair Reid
2018-06-27RTS: Delete __SetConfig stub functionAlastair Reid
This is now directly supported from SAIL so we can call the SAIL __SetConfig function instead.
2018-06-26turn on warnings when compiling mips c then dial back ones that are ↵Robert Norton
triggered by generated code (probably false positives). Fix some warnings in rts.c
2018-06-26RTS: implement sleep primitivesAlastair Reid
Note that an alternative implementation choice is just to implement them as SAIL functions manipulating a global variable. Not sure which is better.
2018-06-26RTS: stub support for -C command line optionAlastair Reid
2018-06-26ELF: Restore error messages in ELF readerAlastair Reid
2018-06-25Coq: add typeclass based comparison, and instantiate for enumsBrian Campbell
2018-06-25Coq: automatic cast introductionBrian Campbell
2018-06-25Use getopt rather than argp for Mac compatibility in C runtimeAlasdair Armstrong
Also further tweaks to Sail library for C and include sail lib files for tracing
2018-06-25flush stdout after putchar for terminal emulation purposes.Robert Norton
2018-06-22Precise bitvector subrange functions for Coq.Brian Campbell
Also fix the constraints in the standard prelude files, add a couple of useful cast rewriting lemmas.
2018-06-22Add coq builtins for MIPSBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-22Coq: project away range types in comparisonsBrian Campbell
2018-06-21Add command line option support for Sail->C compiled modelsAlasdair Armstrong
For example, the MIPS model can boot FreeBSD as ./mips_c --binary=0x100000,/path/to/kernel --image=/path/to/simboot.sailbin Or with short options as ./mips_c -b 0x100000,/path/to/kernel -i /path/to/simboot.sailbin The current options are: -e, --elf, which loads an elf file directly -n, --entry, which sets the entry point -i, --image, which loads an image file compiled by "sail -elf" using Linksem -b, --binary, which loads a plain binary image into memory at a specific address -l, --cyclelimit, which means the (new) cycle_count() builtin exits the model after a certain number of calls Also there are the default -? --help and --usage options.
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-06-21Merge branch 'sail2' of github.com:rems-project/sail into sail2Alasdair Armstrong
2018-06-21add PMP registers to CSR, fix buildJon French
2018-06-21Merge branch 'tracing' into sail2Alasdair Armstrong
2018-06-21Fix MIPS wrt changes to C runtimeAlasdair Armstrong
This plus changes to bitfield internals is enough to run some MIPS tests at 1Mhz.
2018-06-21Simplify the ANF->IR translationAlasdair Armstrong
Previously the ANF->IR translation cared too much about how things were allocated in C, so it had to constantly check whether things needed to be allocated on the stack or heap, and generate different cequences of IR instructions depending on either. This change removes the ialloc IR instruction, and changes iinit and idecl so that the code generator now generates different C for the same IR instructions based on the variable types involved. The next change in this vein would be to merge icopy and iconvert at the IR level so that conversions between uint64_t and large-bitvectors are inserted by the code generator. This would be good because it would make the ANF->IR translation more robust to changes in the types of variables caused by flow-typing, and optimization passes could convert large bitvectors to uint64_t as local changes.
2018-06-20Coq: reverse_endiannessBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: port handling of effectful and/or from Lem backendBrian Campbell
2018-06-20Coq: a few more opsBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell
2018-06-19Add elf parsing from AlastairAlasdair Armstrong
2018-06-19Improvements to Sail C for booting LinuxAlasdair Armstrong
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-15Fixes for C RTS for aarch64 no it's split into multiple filesAlasdair Armstrong
Fix a bug involving indentifers on the left hand side of assignment statements not being shadowed correctly within foreach loops. Make the different between different types of integer division explicit in at least the C compilation for now. fdiv_int is division rounding towards -infinity (floor). while tdiv_int is truncating towards zero. Same for fmod_int and tmod_int.
2018-06-14Refactor C backend, and split RTS into multiple filesAlasdair
2018-06-13Tracing instrumentation for C backendAlasdair Armstrong
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-11More efficient bitfield implementationAlasdair Armstrong
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:46:35 +0000