summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-10-08Support exporting single bit and bool values to external bitvectorsKathy Gray
2014-10-07Connect interpreter to representation of instructions.Kathy Gray
Warning: this changes a few of the constructor names in the instruction_extractor.lem interface
2014-10-07Track dependencies on size of memory accessKathy Gray
2014-10-07kathy,peter: making decode integration with ppcmem2 typecheckPeter Sewell
2014-10-07Actually add the new fileKathy Gray
2014-10-07Merge and make real Peter's comment typeKathy Gray
2014-10-07Put in type for instruction form for models; remove extra information from ↵Kathy Gray
Bytevectors; add place holder for memory size dependency tracking
2014-10-07comment with suggested i_state_or_error typePeter Sewell
2014-10-06Getting closer with non-opam makefileKathy Gray
2014-10-04clarify Step constructorKathy Gray
2014-10-04Add alternative non-opam Makefile in src/.Stephen Kell
2014-10-04configure uint before makeKathy Gray
2014-10-03Add a decoding function to interp_interface and interp_inter_imp. (Note, ↵Kathy Gray
this is quite specific to Power's spec)
2014-10-02correct renaming typoKathy Gray
2014-10-01Add file to download required librariesKathy Gray
2014-10-01Fix bug omitting wmem effectsKathy Gray
2014-09-30Corrected writing to register bug. Now interpreter produces same result as ↵Kathy Gray
gdb on actual binary for hello6
2014-09-30Add type annotations to funcls to track effects and constraints from one ↵Kathy Gray
function-clause
2014-09-30Executing an actual elf fileKathy Gray
2014-09-29Connect up to elf model; which doesn't seem to be representing the elf file ↵Kathy Gray
properly yet but run_power.native is connected to it
2014-09-29add run_power to last commitKathy Gray
2014-09-29Add in elf model from Dominic/Stephen. Make run_power build again. Does not ↵Kathy Gray
effectively use elf model yet
2014-09-19Functions to extract instruction informationKathy Gray
2014-09-11Adding support for extracting the information Christopher needs about an ↵Kathy Gray
instruction
2014-09-10reduce lem macro overhead for sail _ very slightly _Kathy Gray
2014-09-09Small fix to printingKathy Gray
2014-09-09Full power.sail now type checking and generating Lem.Kathy Gray
2014-09-09Get more constraints resolving in power.sailKathy Gray
2014-09-05refinements to constraint checkingKathy Gray
2014-09-04Refine overloading resolution with respect to vectors and rangesKathy Gray
Fix a few other bugs as well
2014-09-04Make exhaust run from the first breakpoint in the interactive interpreterKathy Gray
(I still think this is a silly place to run exhaust from, but it no longer finds errors or crashes)
2014-08-30fix various bugs exposed by armv8Kathy Gray
2014-08-28more bug fixes and adding more library functionsKathy Gray
2014-08-28fixes to bugs exposed by arm modelKathy Gray
2014-08-27Changes to get another (slightly larger) executable running;Kathy Gray
adding executable as a test as well
2014-08-26small changes for armKathy Gray
2014-08-24Use LEM_DIR environment variable if definedGabriel Kerneis
LEM_DIR must contain the *absolute* path the Lem directory. If not defined, the previous behaviour is retained: a relative path is used, assuming Lem is in bitbucket/lem.
2014-08-24Silence some OCaml warningsGabriel Kerneis
2014-08-21Improve printing of function calls in stepper modeKathy Gray
2014-08-21Allow command line interface to exhaustively evaluate the next step, ↵Kathy Gray
printing the events. Note: this commit switches back to a standard lem build located in ~/bitbucket/lem/lem
2014-08-20Add ability to track register dependencies in interactive stepper; thus ↵Kathy Gray
testing register tracking/tainting
2014-08-19make test_power_interactive working again; now using interp_interface ↵Kathy Gray
instead of internal actions
2014-08-19Add file that actually drives command line interpreterKathy Gray
2014-08-18Handling many register reads, writes, and memory reads.Kathy Gray
There are problems that warrant discussion about handling special registers that hold records or data structures previously.
2014-08-18fix compile errorKathy Gray
2014-08-18Switch run_power to use interp_interface. Compilers and begins running, and ↵Kathy Gray
then hits an error. So still in progress Note: moved barrier kind changes to interp_interface, along with other memory kinds
2014-08-18wib?Peter Sewell
2014-08-18make interp_exhaustive not take an interp_mode argumentPeter Sewell
2014-08-18tweak barrier kinds in interface (likely needs changes elsewhere)Peter Sewell
2014-08-14Small tweaks to interp_interface interfaceKathy Gray
Also adding more comments and getting the ml files built in the build process