summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
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-21changes to riscv model to support rmemJon French
2018-06-20Coq: Generate MR when appropriate; syntax fixesBrian Campbell
2018-06-20Coq: add missing existential projection on simple let expressionsBrian Campbell
2018-06-20Coq: Tidy up libraries, export StringBrian Campbell
2018-06-20Coq: print div/mod/abs in nexps; avoid mod as an identifierBrian Campbell
2018-06-20Coq: port handling of effectful and/or from Lem backendBrian Campbell
2018-06-19Minor optimization in ocaml_backend to use ints instead of strings for ↵Prashanth Mundkur
Big_int literals. Improves tests/riscv duration by around 2% and size of riscv.o by 15%.
2018-06-19Coq: use undefined_bitvectorBrian Campbell
2018-06-19Add elf parsing from AlastairAlasdair Armstrong
2018-06-19Improvements to Sail C for booting LinuxAlasdair Armstrong
2018-06-18Coq: better handling of identifiers, esp infix onesBrian 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-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-14provide impl of int_of_string_opt in Sail_lib to support older Ocaml versionsJon French
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: Handle simple top-level type variable definitionsBrian Campbell
(also another error reporting improvement)
2018-06-12Coq: upgrade some errors to report locationsBrian Campbell
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-11add 'pat as id' mapping-patternsJon French
2018-06-11More efficient bitfield implementationAlasdair Armstrong
2018-06-11Merge branch 'sail2' into mappingsJon French
(involved some manual tinkering with gitignore, type_check, riscv)
2018-06-11change double-caret for string-append-pattern to single caret, since that ↵Jon French
wouldn't be legal in a pattern anyway
2018-06-11better type inference of union-constructors and mappingsJon French
2018-06-09Fix issue in C_backend, and run C tests with undefined behavior sanitizerAlasdair
2018-06-09Fix issue with catch block return values not being compiled correctlyAlasdair
This should fix the issue raised in commit 45554f Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations
2018-06-08Fix use of non-tail-recursive calls in elf_loader.Prashanth Mundkur
2018-06-08type checking mappings: allow inferring based on the other side's id inferencesJon French
2018-06-08Coq: some handling of existential types as function return typesBrian Campbell
2018-06-08Coq: add destructuring of atom existentials in patternsBrian Campbell
Plus test case, broken builtin name
2018-06-08Coq: track add_typquant changeBrian Campbell
2018-06-08Correct dependencies of bytecode sailBrian Campbell
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-08Coq: fix axiom generationBrian Campbell
2018-06-08Coq: update foreach handling, correct field accessesBrian Campbell
2018-06-08Coq: correct failure on unsupported undefined valuesBrian Campbell
2018-06-08Coq: use record update syntax (only single fields work for now)Brian Campbell
2018-06-08Coq: correct implicitness of type arguments in unionsBrian Campbell
2018-06-07Fix bug in add_bits optimizationAlasdair Armstrong
2018-06-07Fix a small bug in monomorphisationThomas Bauereiss
2018-06-06Fix a typo.Yao Li
2018-06-07Add a constant folding optimization passAlasdair
2018-06-06Factor utility functions for IR into separate file and struct update ↵Alasdair Armstrong
optimizations. Move the utility functions for graph generation and pretty printing of intermediate representation instructions into a separate file, bytecode_util.ml, by analogy with ast_util.ml. Add an optimization pass that searches for specific patterns of struct updates and removes uncessary copying of the structs involved. With this optimisation pass the time taken for u-boot to run approx 57,000,000 instructions goes down from about 11-12 minutes to 8 minutes (about 120,000 IPS).
2018-06-06Some additional fixes to C backend. Re-enable primitive optimizations.Alasdair Armstrong
Also add an additional -Oz3 flag that uses z3 to optimize some additional types. This is currently very experimental and doesn't fully work yet.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-12 11:41:59 +0000