summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-03-09cheri sail: introduce functions for casting from cap. register to cap. ↵Robert Norton
struct and use cap structs for easier syntax to ensure atomic writes of cap regs.
2016-03-08missing file from last commitKathy Gray
2016-03-08Return undefined value on reads of uninitialised memoryKathy Gray
2016-03-08Fix error in handling type abbreviations in LEXP type checkerKathy Gray
2016-03-08Start task of setting up tagged memory in sequential interpreterKathy Gray
2016-03-08add beginnings of cheri sail for kathy to do some debugging.Robert Norton
2016-03-07Split mips.sail into three file and make use of the new -o option in ↵Robert Norton
preparation for adding cheri support in separate files.
2016-03-03Fix typo in manual which had true instead of false on assert documentationKathy Gray
Fix bug in local register access
2016-03-02Add new language feature to permit definitions of items of kind Nat, etc as ↵Kathy Gray
well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required.
2016-02-26tweak READMEPeter Sewell
2016-02-25A bit better readmeKathy Gray
A few more tips Trying to fix up and bring up to date the built-in types and library
2016-02-25Expand what advice and information is in the manual slightlyKathy Gray
2016-02-25Add the manual, such as it is, for others to be able to use and have without ↵Kathy Gray
needing ott
2016-02-25Restore manual.tex mysteriously deleted by peter in May 2015.Robert Norton
2016-02-25Update read me to the present day and cause the makefile from the top level ↵Kathy Gray
directory to be a bit more sensible
2016-02-25Merge branch 'master' of bitbucket.org:Peter_Sewell/l2Peter Sewell
Conflicts: src/Makefile
2016-02-25defunct commitPeter Sewell
2016-02-24Small mixups to get the initial check infrastructure working for full ast ↵Kathy Gray
processing
2016-02-23Make small tweaks to emacs modeKathy Gray
2016-02-23Several fixesKathy Gray
Improve printing for asl to sail readability; Add -o option for selecting the name of file generation; Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes
2016-02-11mips.sail: add cast to bit to work around type error recently introduced by ↵Robert Norton
overloading of '^^'
2016-02-11point to lem and linksem embedded versions of libraries instead of relying ↵Robert Norton
on opam provided ones.
2016-02-11fix some bugs in emacs mode for sail; mostly workable now although there's ↵Kathy Gray
some annoying indenting on one line functions
2016-02-11Begin adding some new library functions like absolute valueKathy Gray
2016-02-11use paths relative to current makefile for lem and linksem.Robert Norton
2016-02-10mips.sail: make unimplemented/non-existent throw a reserved instruction ↵Robert Norton
exception as per ISA.
2016-02-10mips.sail: add mfc0 support for some cp0 registers even though they aren't ↵Robert Norton
properly implemented as this allows tests to fail gracefully rather than crashing.
2016-02-10mips.sail: use exit whenever SignalException is called.Robert Norton
2016-02-09fix scattered type union source printingKathy Gray
2016-02-08slightly clean up vector type printing and empty effect printing for functionsKathy Gray
2016-02-05fix typo in kathy's last commit.Robert Norton
2016-02-05change signed mod behaviour for numbers to match that of vectorsKathy Gray
2016-02-04Cast to int in DIV instructions to avoid weird undefined results from vector ↵Robert Norton
quot and mod. mod still not quite doing what we want in signed case.
2016-02-04mips.sail: don't set HI and LO to undefined on MUL but just leave them as ↵Robert Norton
they were, allowing us to pass another test.
2016-02-04fix pretty printing of new mod_sRobert Norton
2016-02-04add mod_s to lexer and parserKathy Gray
2016-02-04Add mod_sKathy Gray
2016-02-04add forgotten lib bindingKathy Gray
2016-02-04and for quot_sKathy Gray
2016-02-04Relax constraints on quot temporarily since it was prohibiting negative ↵Kathy Gray
numbers accidentally
2016-02-03mips: finish implementing address translation on instruction fetch and ↵Robert Norton
remove temporary hack in TranslateAddr.
2016-02-03mips: add support for LLAddr, a debug register used for ll/sc. Also add ↵Robert Norton
missing psuedo-registers in run_with_elf.
2016-02-03add example of elf file which fails to load due to linksem error: ↵Robert Norton
get_elf64_global_symbol_init: invariant failed, global variable appears in multiple segments
2016-02-03mips_extras.lem: fix typo in spelling of MEM_sync.Robert Norton
2016-02-02mips.sail: workaround for sail bugRobert Norton
2016-02-02mips.sail: add an 'inBranchDelay' register so that SignalException can set ↵Robert Norton
correct state on exception. branchPending does not work because it is cleared before executing the branch delay.
2016-02-02mips.sail: TranslateAddress hack maps all xkphys addresses to 0x9... regionRobert Norton
2016-02-02Print out the address of the instruction running in sequential interpreterKathy Gray
2016-02-02Get mips stuff hooked up with translate address.Kathy Gray
Note: this support is rather mips centric at the moment
2016-02-02add translate_address functionalityKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 01:10:25 +0000