summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2016-07-25one more goKathy Gray
2016-07-25Actually fix stack for returnKathy Gray
2016-07-25Fix stack for returnKathy Gray
2016-07-25Support return in interpreter pretty printer (also fix typo for default case)Kathy Gray
2016-07-25auto coerce to bit vector from bitKathy Gray
pretty print lret effects into lem
2016-07-24Make sure that all type constructors with unit type have a type union with ↵Kathy Gray
just an id (hopefully fixes Christopher issue).
2016-07-23Add effect annotation for return, and actually keep a return after type check.Kathy Gray
2016-07-23Add a return exp form to Sail, supported in type checker and in interpreter.Kathy Gray
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-07-20Make rewriter understand type abbreviations for removing internal_exp instancesKathy Gray
2016-07-13fixesChristopher
2016-07-12sail-to-lem and lem library fixesChristopher
2016-07-01Add missing case to arith_op_no0Kathy Gray
Add type refinement to arm spec
2016-06-20Fix error in type checker that put some constraints wrongly into conditional ↵Kathy Gray
constraints, breaking power. Also improve reporting of contract constraints, but then turn them off :( to allow power to compile.
2016-06-07Fix issue in accessing fields and slices of registers during translate addressKathy Gray
2016-06-07add a test for failing TLB translation during instruction fetch.Robert Norton
2016-06-06remove mips test elf files no longer expected to work due to having ↵Robert Norton
incorrect LMA values (since sail interpreter now translates PC addresses).
2016-06-06add test for failing tlb translation using current sail.Robert Norton
2016-06-03Fix bug exposed/introduced by properly handling vector starts in the type ↵Kathy Gray
checker
2016-06-03Change path inside sail Makefile to look for sail directory instead of l2Kathy Gray
2016-06-03turn off debug print statementsKathy Gray
2016-06-03Mips file: removed some unnecessary parenthesisKathy Gray
Interp: trying to add some debugging to isolate bug
2016-06-03Add test demonstrating recently introduced regression where tlb match fail.Robert Norton
2016-06-02Fix most_significant case omissionKathy Gray
2016-06-02Get widening right now that it mattersKathy Gray
2016-06-02improve constraint range checkingKathy Gray
2016-05-27Fix parsing of sizeof and some printing issues with letKathy Gray
2016-05-27small change to comment printingKathy Gray
2016-05-27Add sizeof to sail. Documentation to followKathy Gray
2016-05-26add makery for mips/cheir LOC count.Robert Norton
2016-05-25add support for capability load/store bits in TLBRobert Norton
2016-05-20Add missing CP0BadVaddr in run_with_elfs.Robert Norton
2016-05-18Implement 8-entry software-managed TLB.Robert Norton
2016-05-12Implement count/compare registers for timer interrupts and rdhwr instruction.Robert Norton
2016-05-10Initialise CP0Status BEV bit.Robert Norton
2016-05-09fix mips build by copying across run_with_elf_cheri.ml and removing cheri parts.Robert Norton
2016-05-09Reverse the list of events to respect their orderKathy Gray
2016-05-09commit test which fails due to not writing C31.offset in TranslateAddress.Robert Norton
2016-05-09Add more debugging information for vector concatenationKathy Gray
2016-05-06rewrite fde_loop to make it easier to understand and fix some tests. still ↵Robert Norton
requires some clean up (currently one huge function).
2016-05-05Factor out get_opcodeRobert Norton
2016-05-04Correct register field/slice reading for decreasing reads for ↵Kathy Gray
decode/translate_address/exhaustive. (Was previously correct for full register reads)
2016-05-03List registers required to handle exception during instruction fetch. ↵Robert Norton
Attempt to get correct behaviour wrt nextpC on instruction fetch exception (prob. still wrong).
2016-05-03actually read next_pc twice when handling a translate_address exceptionKathy Gray
2016-05-03write all or part of fields out of translate_address (instead of just all)Kathy Gray
fix bug in interp_to_value_helper
2016-05-03Change decode and translate_address to support writing register events ↵Kathy Gray
(although decode isn't pushed through yet). Note: this will break all builds
2016-04-27slightly simplify set_next_instruction_address -- no need to read convert ↵Robert Norton
then reconvert delayedPC
2016-04-27expand supported patterns for most_significantKathy Gray
2016-04-27Make run_with_elf compile againKathy Gray
2016-04-27cheri: add translation and bounds checking of PC via PCC. Slightly clunky ↵Robert Norton
implementation for now and exceptions not properly handled.
2016-04-26Add more cases for translate_address to support enumsKathy Gray