diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 18 |
1 files changed, 14 insertions, 4 deletions
@@ -202,7 +202,9 @@ src directory (including some generated files) ast.ml symlink to language/l2.ml demo.sh script for setting up a demo finite_map.ml utility implementation +gen_lib/ source directory of libaries used by generated back ends initial_check.ml translate l2_parse grammar to l2 grammar +initial_check_full.ml performs sames checks as above as to kind well-formedness but over l2 grammar lem_interp/ source directory of interpreter lexer.mll myocamlbuild.ml @@ -212,14 +214,14 @@ pp.ml utility for printing pprint/ library directory of someone else's pretty printing combinators pre_lexer.mll First pass lexer, to identify type identifiers pre_parser.mly First pass parser, to identify type identifiers for actual parsing -pretty_print.ml our printers; one to Sail source, one to Lem ast +pretty_print.ml our printers; one to Sail source, one to Lem ast, one to Lem, and one to Ocaml process_file.ml reporting_basic.ml -run_power.native executable for interpreting power model with simple memory -run_tests.native executable to run test suite +rewriter.ml performs sail-to-sail transformations for various back ends sail.ml main file sail.native executable for Sail sail_lib.ml treat some sail functions as a library, for idl/power generation +spec_analysis.ml analyses a fully type annotated ast, primarily used by rewriters test/ directory of test suite type_check.ml Main type checker type_internal Structure of internal types, and type - type comparisons @@ -232,11 +234,19 @@ make run_mips.native Builds an executable sequential interpreter for MIPS Elf bi make clean lem_interp directory +instruction_extractor.lem processes a specification and identifies the ast nodes of instructions with appropriate tags to convert data types into/out of sail value type interp.lem interpreter implementation interp_ast.lem symlink to language/l2.lem interp_inter_imp.lem implementation of externally visible interface interp_interface.lem externally visible interface for memory interp_lib.lem implementation of sail library functions +interp_utilities.lem commonly useful functions for interpreter +sail_impl_base.lem externally visible interface above interp_interface pretty_interp.ml pretty printing for interperter forms -run_interp.ml interactive implementation for running interpreter with simple memory and registers +run_interp.ml interactive implementation for running interpreter with simple memory and registers, bitrotted +run_interp_model.ml interactive implementation for running sequential binaries +run_with_elf.ml hook run_interp_model up with elf support, main file of sequential interpreter +run_with_elf_cheri.ml as above but specific to cheri +run_with_elf_cheri128.ml +type_check.lem implementation to type check fully inferenced, annotated, ast nodes (not complete) |