summaryrefslogtreecommitdiff
path: root/src/lem_interp/sail_impl_base.lem
AgeCommit message (Collapse)Author
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
The type-checker already supports a user-defined "exception" type that can be used in throw and try-catch expressions. This patch adds support for that to the Lem shallow embedding by adapting the existing exception mechanisms of the state and prompt monads. User-defined exceptions are distinguished from builtin exception cases. For example, the state monad uses type ex 'e = | Exit | Assert of string | Throw of 'e to distinguish between calls to "exit", failed assertions, and user-defined exceptions, respectively. Early return is also handled using the exception mechanism, by lifting to a monad with "either 'r exception" as the exception type, where 'r is the expected return type and "exception" is the user-defined exception type.
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
- Add support for some internal nodes to type checker - Add more explicit type annotations during rewriting - Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer; these will be resolved by the type checker during rewriting now
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-01added RISC-V "fence r,r"Shaked Flur
2017-10-25Alternative low-memory version of barrier_kindCompareBrian Campbell
2017-09-29fix deep_shallow_convert, stop using interp_interface.instruction for most ↵Christopher Pulte
things, SF and CP bugfixing
2017-09-21added a comment to the x86 lock'd read and writeShaked Flur
2017-09-20add support for x86 lock prefix (also remove unused Read/Write_tag kind in ↵Robert Norton
etc/regfp.sail.
2017-09-15reinstate deep/shallow conversionChristopher Pulte
2017-09-03added RISC-V strong-acquire/releaseShaked Flur
2017-08-31add EnumerationType type class: if a type is a member you get Ord membership ↵Christopher Pulte
and Set membership for free
2017-08-31added RISC-V AMOsShaked Flur
2017-08-30typeclass instance Ord(opcode)Christopher Pulte
2017-08-28Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments # Conflicts: # src/gen_lib/sail_values.lem
2017-08-24Begin refactoring Sail libraryThomas Bauereiss
- Add back support for bit list representation of bit vectors, for backwards compatibility in order to ease integration with the interpreter. For this purpose, split out a file sail_operators.lem from sail_values.lem, and add a variant sail_operators_mwords.lem for the machine word representation of bitvectors. Currently, Sail is hardcoded to use machine words for the sequential state monad, and bit lists for the free monad, but this could be turned into a command line flag. - Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem library. The wrappers make use of sizeof expressions to extract type information from bitvectors (length, start index) in order to pass it to the Lem functions. - Add early return support to the free monad, using a new constructor "Return of 'r". As with the sequential monad, functions with early return are wrapped into "catch_early_return", which extracts the return value at the end of the function execution.
2017-08-24typoShaked Flur
2017-08-24typoShaked Flur
2017-08-24added barrier-kind for x86 MFENCE;Shaked Flur
fixed some compare functions;
2017-08-22added RISC-V "fence w,w" and "fence.i";Shaked Flur
fixed the interpreter nias analysis;
2017-08-19RISC-V store-releaseShaked Flur
2017-08-17added RISC-V load-acquireShaked Flur
2017-08-17fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w")Shaked Flur
2017-05-24Merge branch 'master' of bitbucket.org:Peter_Sewell/sailShaked Flur
# Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-05-24Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵Robert Norton
data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
2017-05-02docPeter Sewell
2017-04-24added register_value_for_regShaked Flur
2017-04-18added transactional memory supportShaked Flur
2017-03-24fixed endiannessShaked Flur
2017-03-23the interpreter/shallow expects little-endian memory-valuesShaked Flur
2017-02-08put back the header into Sail_impl_baseChristopher Pulte
2017-02-08pull in Shaked's type class instance changes, fix Ord and Eq instancesChristopher Pulte
2017-02-03fix headersPeter Sewell
2017-01-24functionality for comparing handwritten analysis function with exhaustive ↵Christopher Pulte
interpreter
2017-01-14changes to enable interpreter exhaustive analysis in ppcmem againChristopher Pulte
2016-12-09sail changes for making lem embedding Isabelle-friendlierChristopher Pulte
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
2016-11-30add new barrier kind for MIPS (only one for now).Robert Norton
2016-11-27make outcome_s contain the instruction state pretty print rather than the ↵Christopher Pulte
instruction state, factor out interpreter/shallow embedding value conversion
2016-11-09move decode_error type back to Sail_impl_base for nowChristopher Pulte
2016-11-08fixesChristopher Pulte
2016-11-07factor out regfp analysis types into etc/regfp.sailChristopher Pulte
2016-11-05fixesChristopher Pulte
2016-10-25shallow embedding fixesChristopher Pulte
2016-10-24fixes, check in Shaked's sail_impl_base changesChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-19remove effect list from instruction typeChristopher Pulte
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 20:45:39 +0000