summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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
2014-08-13Update library functionsKathy Gray
2014-08-13FInd/fix a redundant case now that warnings are manageableKathy Gray
2014-08-13Silence some lem warnings in compilation.Kathy Gray
2014-08-13Complete tainting phase 1Kathy Gray
Now when mode.track_values is true, on every register read, the returned value is tainted with the register it came from. This tracking is followed through every operation the interperter touches (except library functions, to be completed next). One a memory operation involving a tracked value, there is optionally list of registers that value arose from in the memory request (i.e. maybe (list reg_name)).
2014-08-13Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to ↵Peter Sewell
temporarily use other version of Lem
2014-08-12taint tracking through most of interpreterKathy Gray
Need to add cases for tracking a taint past a conditional check where possible; and then to actually generate them from reading registers.
2014-08-12more taint tracking, yet againKathy Gray
2014-08-11More taint tracking.Kathy Gray
Catch interp_inter_imp up with interp. WARNING: This commit triggers an exponential performance bug in Lem. To alleviate this bug, I am running with a locally modified Lem that has line 1321 of lem/src/typed_ast.ml commented out (On my laptop, I gave up trying to compile after about 900 seconds; beefier computers May be able to run unmodified, I don't know)
2014-08-09More tracking register dependency; another check point that compiles in ↵Kathy Gray
under two minutes
2014-08-08Tracking register dependence.Kathy Gray
Check point where Lem will compile interpreter in under 2 minutes
2014-08-07Fix bug introduced by last commitKathy Gray
2014-08-07Track taints across machine calls.Kathy Gray
This introduced a bug in vector.sail, commented out and needs to be fixed.
2014-08-05start tainting values with register dependenciesKathy Gray
2014-08-05missed file from last commitKathy Gray
2014-08-05Support extracting length information into more functionsKathy Gray
2014-08-03Improve types for checking power.sailKathy Gray
2014-08-01Add some more types for power.sail generation.Kathy Gray
2014-08-01Support separated memory read/write functions.Kathy Gray
Also allows register writing functions to be on the left hand side of an assignment in the same way. The last parameter to a writing function is the value to be written, and should appear on the right hand side of an assignment expression.
2014-07-31start separating memory reads and writesKathy Gray
2014-07-30working dec vectorsKathy Gray
2014-07-29A file can now declare that a default order is either inc or dec, and this ↵Kathy Gray
will be reflected in short hand type syntax, inc is still the default if undeclared So: default order dec register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *) default order inc register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *) It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon.
2014-07-25Add another type signature needed (we think but Susmit and I can't quite ↵Kathy Gray
remember why) for ppcmem integration.
2014-07-25Update make file to make clean from top level directory, and to not build ↵Kathy Gray
all tests on all. Instead there is a make full command to make all the tests as well as everything.
2014-07-25Additional functions for interfaceKathy Gray
2014-07-18Writing to concatenated aliasesKathy Gray
2014-07-16Reading from an alias to two concatenated registers; not writing yet.Kathy Gray
2014-07-16Get writing working for aliases in the interpreter, other than concatenation.Kathy Gray
2014-07-15Type check alias use in the left hand side of an assignment. Warning, ↵Kathy Gray
interpreter still doesn't work with writes.
2014-07-15Finishing up some of the support for ExitKathy Gray
2014-07-15Add failing test for type of aliasesGabriel Kerneis
File "test/regbits.sail", line 23, character 3 to line 23, character 4 Type error: Can only assign to identifiers with type register or reg, found identifier CA with type bit
2014-07-14Add register to alias concatenation typeKathy Gray
2014-07-14Alias pretty-printingGabriel Kerneis
2014-07-14Initial support for aliases and exit through the type system and the ↵Kathy Gray
interpreter. An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
2014-07-08add additional cases for nexp normalisationKathy Gray
2014-07-04Relax constraints for quot_vecGabriel Kerneis
2014-07-04Correct error of forgetting type information that was allowing more programs ↵Kathy Gray
than it should have