summaryrefslogtreecommitdiff
path: root/aarch64_small
AgeCommit message (Collapse)Author
2020-11-25Fix BLRShaked Flur
Reorder the read and write of registers to allow MP+dmb.sy+blr-addr.
2020-11-25Make WFE, SEV and SEVL effectively NOPsShaked Flur
2019-08-20add -coq_alt_modules option to override the default imported modulespes20
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
Fix SMT mem_builtin test case
2019-07-18Update aarch64_small to build with new barriersAlasdair Armstrong
Make sure barrier changes don't affect other models for now
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-16Fix all remaining tests for this branchAlasdair
2019-06-24Rules and supporting files for building aarch64_small monomorphised IsabelleBrian Campbell
2019-06-20Tweak two aarch64_small definitions to help monomorphisationBrian Campbell
2019-06-06SMT: Rename some functions to make usage clearerAlasdair Armstrong
2019-06-06Fix aarch64_small makefileAlasdair Armstrong
2019-06-06Add an option to pre-compile the axiomatic model for SMTAlasdair Armstrong
2019-06-06Update aarch64_small hgen filesAlasdair Armstrong
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
Add a test case for this
2019-05-13aarch64_small: correct cast_bool_bit/cast_bit_bool functionsJon French
Fixes issue with spurious alignment faults etc.
2019-05-13aarch64_small: convert memory access functions to use sail2 primitivesJon French
2019-05-13aarch64_small: remove spurious extra declaration of _rPCJon French
2019-05-13aarch64_small: convert armv8_extras_embed.lem to new types etcJon French
2019-05-13aarch64_small: extern-ify and implement TMCommitEffect and SCTLR converterJon French
2019-05-13aarch64_small: fix interpreter primops in preludeJon French
2019-05-13aarch64_small: sort out types and names in hgen filesJon French
2019-05-13aarch64_small: move around Unreachable fns to sort dependency issueJon French
2019-05-13aarch64_small: correct a couple of incorrect effectsJon French
2019-05-13aarch64_small: add to Makefile parts for RMEMJon French
2019-03-22Tidy up of div and mod operators (C implementation was previously ↵Robert Norton
inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.
2019-03-08wibShaked Flur
2019-03-08Adds the DC and IC instructions to AArch64_small;Shaked Flur
Also, removes etc/regfp.sail and etc/regfp2.sail in favour of lib/regfp.sail
2019-03-05Add missing comma in armV8.sailAlasdair Armstrong
2019-03-05Add Unallocated to the gen filesBen Simner
Adds the Unallocated sail ast node to be tracked by all the transformation files, to track the change made to sail1.
2019-03-04cleanupChristopher Pulte
2019-03-04last bit of sail1 to sail2 portingChristopher Pulte
2019-03-04more sail1-to-sail2 portingChristopher Pulte
2019-03-04more porting of armv8 from sail1 to sail2Christopher Pulte
2019-03-04moreChristopher Pulte
2019-03-02moreChristopher Pulte
2019-03-02moreChristopher Pulte
2019-03-02moreChristopher Pulte
2019-03-01more progressChristopher Pulte
2019-02-28more progressChristopher Pulte
2019-02-13fixesChristopher Pulte
2019-02-13small progressChristopher Pulte
2019-02-12checking in in-progress translation of Shaked's handwritten sail1 ARM model ↵Christopher Pulte
to sail2
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:06:02 +0000