diff options
| author | Peter Sewell | 2017-02-05 11:27:49 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-02-05 11:27:49 +0000 |
| commit | bd384860e2778fe40e10aaf08cdea7d42dae6287 (patch) | |
| tree | f1c88810d0acd8d6360a8b74d21aed689845884c | |
| parent | 081d3ac6a786fdc3df515de58af2ef25a25a5b58 (diff) | |
| parent | 0f688281254997cb4ca3a6e82275c3751c43fe2c (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/sail
Conflicts:
language/manual.pdf
85 files changed, 4300 insertions, 678 deletions
@@ -1,12 +1,7 @@ -.PHONY: all sail language clean archs +.PHONY: all sail language clean archs apply_header all: sail interpreter -apply_header: - headache -c etc/headache_config -h etc/mips_header `ls mips/*.sail` - headache -c etc/headache_config -h etc/mips_header `ls cheri/*.sail` - $(MAKE) -C arm apply_header - sail: $(MAKE) -C src ln -f -s src/sail.native sail @@ -17,13 +12,24 @@ language: interpreter: $(MAKE) -C src interpreter +archs: + for arch in arm mips cheri; do\ + $(MAKE) -C "$$arch" || exit;\ + done + +apply_header: + $(MAKE) clean + headache -c etc/headache_config -h etc/mips_header `ls mips/*.sail` + headache -c etc/headache_config -h etc/mips_header `ls cheri/*.sail` + headache -c etc/headache_config -h src/LICENCE `ls src/Makefile*` + headache -c etc/headache_config -h src/LICENCE `ls src/*.ml*` + headache -c etc/headache_config -h src/LICENCE `ls src/lem_interp/*.ml` + headache -c etc/headache_config -h src/LICENCE `ls src/lem_interp/*.lem` + $(MAKE) -C arm apply_header + clean: for subdir in src arm ; do\ $(MAKE) -C "$$subdir" clean;\ done - rm sail + -rm sail -archs: - for arch in arm mips cheri; do\ - $(MAKE) -C "$$arch" || exit;\ - done @@ -13,6 +13,8 @@ specification language: - a Sail specification of a MIPS ISA (in mips/) +- a Sail specification of a Cheri ISA (in cheri/) + - a Sail specification of part of the ARMv8 ISA (in arm/) - a sequential Sail interpreter, which evaluates an ELF binary for an @@ -52,9 +54,9 @@ then one may also want to run executables sequentially, to debug the specification and begin testing. For this, there is the sequential sail interpreter, which evaluates the specification on an ELF file. At present, doing this for a new architecture will require conversation -with Kathy Gray, as the connections within the sail interpreter -implementation to the architecture being simulated have not been -factored out into external specification files. +with Robert Norton Wright or Kathy Gray, as the connections within +the sail interpreter implementation to the architecture being simulated +have not been factored out into external specification files. Building the architecture for compilation to connect to the interpreter, one uses the sail executable: @@ -65,7 +67,6 @@ which will generate a mips.lem file in the current directory, which will be linked with the sail interpreter (the output is a verbose representation of the sail AST). -*** In progress. Does not work yet *** To generate Lem specifications for theorem proving, one uses the sail executable with flag: ./sail mips/mips.sail -lem @@ -83,7 +84,7 @@ SAIL COMPILER The Sail compiler requires OCaml; it is tested on version 4.02.3. Run "make" in the top level sail directory; this will generate an executable -called sail in this directory. +called sail in this directory and will compile the interpreter files. make clean will remove this executable as well as the build files in subdirectories. @@ -102,7 +103,7 @@ The Sail interpreter relies on external access to two external tools: a public Bitbucket repository https://bitbucket.org/Peter_Sewell/linksem -The Sail build system expects to find these repositories in in the same +The Sail build system expects to find these repositories in the same directory as the sail repository by default. This can be changed with make variables LEM, LEMLIBOCAML, and ELFDIR @@ -162,8 +163,24 @@ Will generate the files spec.lem and spec.ml in the current directory It is not recommended to try to read the generated Lem ast file, as it is a very verbose representation of the AST. -IN PROGRESS COMMANDS: -lem -ocaml -The resulting output of these commands may well be untype checkable Lem or OCaml +IN PROGRESS COMMANDS: -ocaml +The resulting output of these commands may well be untype checkable OCaml + + +****************************************************************************** +LICENCES + +The Sail implementation, in src/, is distributed under the 2-clause +BSD licence in the headers of those files and in src/LICENCE, with the +exception of the library src/pprint, which is distributed under the +CeCILL-C free software licence in src/pprint/LICENSE. + +The ARMv8 model, in arm/, is distributed under the 2-clause BSD +licence in the headers of those files. + +The MIPS and CHERI models, in mips/ and cheri/, are distributed under +the 2-clause BSD licence in the headers of those files. + ****************************************************************************** @@ -176,6 +193,7 @@ Top level directories src/ ML implementation of Sail frontend, Sail executable, subdirectories language/ Ott definitions of source language, pdfs as well mips/ Sail definition of a MIPS specification +cheri/ Sail definition of a Cheri specification risc-v/ abandoned very partial attempt at RISC V specification l3-to-l2/ abandoned but not GC-ed directory @@ -184,6 +202,7 @@ l2_parse.ott Grammar of Sail generated by parser, superset of source language l2.ott Grammar of Sail source l2_typ.ott Grammar of Internal structures used for type annotations l2_rules.ott Rules for type system +manual.tex Source of manual Relevant make commands: make Builds pdfs for l2 and l2_parse, ml and lem files of grammars @@ -199,7 +218,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 @@ -209,14 +230,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 @@ -229,11 +250,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) diff --git a/arm/Makefile b/arm/Makefile index 99c7998f..641a907e 100644 --- a/arm/Makefile +++ b/arm/Makefile @@ -1,6 +1,6 @@ BUILDDIR=./build -SAIL=../sail +SAIL=../sail -verbose ifeq ("$(wildcard $(SAIL))","") $(warning can not find Sail) endif diff --git a/arm/armV8.h.sail b/arm/armV8.h.sail index 01927fbe..c788855a 100644 --- a/arm/armV8.h.sail +++ b/arm/armV8.h.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8.sail b/arm/armV8.sail index 298a6a8c..10c57d1e 100644 --- a/arm/armV8.sail +++ b/arm/armV8.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8_A32_sys_regs.sail b/arm/armV8_A32_sys_regs.sail index 8b4a8e00..40306a20 100644 --- a/arm/armV8_A32_sys_regs.sail +++ b/arm/armV8_A32_sys_regs.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8_A64_lib.sail b/arm/armV8_A64_lib.sail index bb049344..5a1b6ec3 100644 --- a/arm/armV8_A64_lib.sail +++ b/arm/armV8_A64_lib.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8_A64_special_purpose_regs.sail b/arm/armV8_A64_special_purpose_regs.sail index 47e910bd..94d1c079 100644 --- a/arm/armV8_A64_special_purpose_regs.sail +++ b/arm/armV8_A64_special_purpose_regs.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8_A64_sys_regs.sail b/arm/armV8_A64_sys_regs.sail index 90228da1..50c150c6 100644 --- a/arm/armV8_A64_sys_regs.sail +++ b/arm/armV8_A64_sys_regs.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8_common_lib.sail b/arm/armV8_common_lib.sail index 1aa55992..3bae8070 100644 --- a/arm/armV8_common_lib.sail +++ b/arm/armV8_common_lib.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8_lib.h.sail b/arm/armV8_lib.h.sail index 6c8f9aaa..849472e1 100644 --- a/arm/armV8_lib.h.sail +++ b/arm/armV8_lib.h.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/arm/armV8_pstate.sail b/arm/armV8_pstate.sail index da707b44..85e5e797 100644 --- a/arm/armV8_pstate.sail +++ b/arm/armV8_pstate.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Shaked Flur *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Shaked Flur *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 525ff324..5882ec77 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) @@ -83,7 +83,7 @@ function clause execute (CGetBase(rd, cb)) = raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := getCapBase(capVal); + wGPR(rd) := (bit[64]) (getCapBase(capVal)); (* END_CGetBase *) } @@ -95,7 +95,7 @@ function clause execute (CGetOffset(rd, cb)) = raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := getCapOffset(capVal); + wGPR(rd) := (bit[64]) (getCapOffset(capVal)); (* END_CGetOffset *) } @@ -108,8 +108,7 @@ function clause execute (CGetLen(rd, cb)) = else let capVal = readCapReg(cb) in let len65 = getCapLength(capVal) in - let len64 = if unsigned(len65) > MAX_U64 then - (bit[64]) MAX_U64 else len65[63..0] in + let len64 = (bit[64]) (min(MAX_U64, len65)) in wGPR(rd) := len64; (* END_CGetLen *) } @@ -249,7 +248,7 @@ function clause execute(CToPtr(rd, cb, ct)) = wGPR(rd) := if not (cb_val.tag) then ((bit[64]) 0) else - (bit[64])(getCapCursor(cb_val) - unsigned(getCapBase(ct_val))) + (bit[64])(getCapCursor(cb_val) - getCapBase(ct_val)) } (* END_CToPtr *) } @@ -383,8 +382,8 @@ function clause execute (CSetBounds(cd, cb, rt)) = cb_val := readCapReg(cb); rt_val := unsigned(rGPR(rt)); cursor := getCapCursor(cb_val); - base := unsigned(getCapBase(cb_val)); - top := unsigned(getCapTop(cb_val)); + base := getCapBase(cb_val); + top := getCapTop(cb_val); newTop := cursor + rt_val; if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) @@ -414,8 +413,8 @@ function clause execute (CSetBoundsExact(cd, cb, rt)) = cb_val := readCapReg(cb); rt_val := unsigned(rGPR(rt)); cursor := getCapCursor(cb_val); - base := unsigned(getCapBase(cb_val)); - top := unsigned(getCapTop(cb_val)); + base := getCapBase(cb_val); + top := getCapTop(cb_val); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -564,7 +563,8 @@ function clause execute (CSeal(cd, cs, ct)) = cs_val := readCapReg(cs); ct_val := readCapReg(ct); ct_cursor := getCapCursor(ct_val); - ct_top := unsigned(getCapTop(ct_val)); + ct_top := getCapTop(ct_val); + ct_base := getCapBase(ct_val); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cs)) then @@ -581,6 +581,8 @@ function clause execute (CSeal(cd, cs, ct)) = raise_c2_exception(CapEx_SealViolation, ct) else if not (ct_val.permit_seal) then raise_c2_exception(CapEx_PermitSealViolation, ct) + else if (ct_cursor < ct_base) then + raise_c2_exception(CapEx_LengthViolation, ct) else if (ct_cursor >= ct_top) then raise_c2_exception(CapEx_LengthViolation, ct) else if (ct_cursor > max_otype) then @@ -621,7 +623,9 @@ function clause execute (CUnseal(cd, cs, ct)) = raise_c2_exception(CapEx_TypeViolation, ct) else if not (ct_val.permit_seal) then raise_c2_exception(CapEx_PermitSealViolation, ct) - else if (ct_cursor >= unsigned(getCapTop(ct_val))) then + else if (ct_cursor < getCapBase(ct_val)) then + raise_c2_exception(CapEx_LengthViolation, ct) + else if (ct_cursor >= getCapTop(ct_val)) then raise_c2_exception(CapEx_LengthViolation, ct) else writeCapReg(cd, {cs_val with @@ -641,6 +645,7 @@ function clause execute (CCall(cs, cb)) = checkCP2usable(); cs_val := readCapReg(cs); cb_val := readCapReg(cb); + cs_cursor := getCapCursor(cs_val); if (register_inaccessible(cs)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) else if (register_inaccessible(cb)) then @@ -659,7 +664,9 @@ function clause execute (CCall(cs, cb)) = raise_c2_exception(CapEx_PermitExecuteViolation, cs) else if (cb_val.permit_execute) then raise_c2_exception(CapEx_PermitExecuteViolation, cb) - else if (getCapCursor(cs_val) >= unsigned(getCapTop(cs_val))) then + else if (cs_cursor < getCapBase(cs_val)) then + raise_c2_exception(CapEx_LengthViolation, cs) + else if (cs_cursor >= getCapTop(cs_val)) then raise_c2_exception(CapEx_LengthViolation, cs) else raise_c2_exception(CapEx_CallTrap, cs); @@ -704,7 +711,8 @@ function clause execute(CJALR(cd, cb, link)) = checkCP2usable(); cb_val := readCapReg(cb); cb_ptr := getCapCursor(cb_val); - cb_top := unsigned(getCapTop(cb_val)); + cb_top := getCapTop(cb_val); + cb_base:= getCapBase(cb_val); if (link & register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -717,7 +725,9 @@ function clause execute(CJALR(cd, cb, link)) = raise_c2_exception(CapEx_PermitExecuteViolation, cb) else if not (cb_val.global) then raise_c2_exception(CapEx_GlobalViolation, cb) - else if (cb_ptr + 4 > cb_top) then + else if (cb_ptr < cb_base) then + raise_c2_exception(CapEx_LengthViolation, cb) + else if ((cb_ptr + 4) > cb_top) then raise_c2_exception(CapEx_LengthViolation, cb) else if ((cb_ptr mod 4) != 0) then SignalException(AdEL) @@ -730,7 +740,7 @@ function clause execute(CJALR(cd, cb, link)) = writeCapReg(cd, linkCap) else assert(false, None); - delayedPC := getCapOffset(cb_val); + delayedPC := (bit[64]) (getCapOffset(cb_val)); delayedPCC := capStructToCapReg(cb_val); branchPending := 1; } @@ -773,9 +783,9 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset)); vAddr64:= (bit[64]) vAddr; - if ((vAddr + size) > unsigned(getCapTop(cb_val))) then + if ((vAddr + size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then + else if (vAddr < getCapBase(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if not (isAddressAligned(vAddr64, width)) then SignalExceptionBadAddr(AdEL, vAddr64) @@ -830,9 +840,9 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset)); vAddr64:= (bit[64]) vAddr; - if ((vAddr + size) > unsigned(getCapTop(cb_val))) then + if ((vAddr + size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then + else if (vAddr < getCapBase(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if not (isAddressAligned(vAddr64, width)) then SignalExceptionBadAddr(AdES, vAddr64) @@ -893,9 +903,9 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (16 * signed(offset)); vAddr64:= (bit[64]) vAddr; - if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then + if ((vAddr + cap_size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then + else if (vAddr < getCapBase(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if ((vAddr mod cap_size) != 0) then SignalExceptionBadAddr(AdES, vAddr64) @@ -942,9 +952,9 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) = cursor := getCapCursor(cb_val); vAddr := cursor + unsigned(rGPR(rt)) + (16*signed(offset)); vAddr64:= (bit[64]) vAddr; - if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then + if ((vAddr + cap_size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) - else if (vAddr < unsigned(getCapBase(cb_val))) then + else if (vAddr < getCapBase(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if ((vAddr mod cap_size) != 0) then SignalExceptionBadAddr(AdEL, vAddr64) diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index a96949a5..f97842a0 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) @@ -105,7 +105,7 @@ function CapStruct capRegToCapStruct((CapReg) c) = permit_execute = c[114]; global = c[113]; reserved = c[112..111]; - E = c[110..105]; + E = c[110..105] ^ 0b110000; sealed = s; B = B; T = T; @@ -132,7 +132,7 @@ function (bit[128]) capStructToMemBits((CapStruct) cap) = ( cap.uperms : getCapHardPerms(cap) : cap.reserved - : cap.E + : (cap.E ^ 0b110000) (* XXX brackets required otherwise sail interpreter error *) : [cap.sealed] : b : t @@ -155,7 +155,7 @@ function (bit[31]) getCapPerms((CapStruct) cap) = function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = { cap with uperms = perms[18..15]; -(* perm_reserved11_14 = (cap.perm_reserved11_14 & (perms[14..11]));*) + (* 14..11 reserved -- ignore *) access_system_regs = perms[10]; perm_reserved9 = perms[9]; perm_reserved8 = perms[8]; @@ -175,51 +175,49 @@ function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) = else (false, undefined) -function int a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) = - switch (a_mid < R, bound < R) { - case (False, False) -> 0 - case (False, True) -> 1 - case (True, False) -> -1 - case (True, True) -> 0 +function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) = + switch (unsigned(a_mid) < unsigned(R), unsigned(bound) < unsigned(R)) { + case (bitzero, bitzero) -> 0 + case (bitzero, bitone) -> 1 + case (bitone, bitzero) -> -1 + case (bitone, bitone) -> 0 } -function bit[64] getCapBase((CapStruct) c) = - let ([|63|]) E = unsigned(c.E) in - let (bool) s = c.sealed in +function uint64 getCapBase((CapStruct) c) = + let ([|45|]) E = min(unsigned(c.E), 45) in let (bit[20]) B = c.B in let (bit[64]) a = c.address in - let (bit[20]) R = B - 0x00100 in (* wraps *) + let (bit[20]) R = B - 0x01000 in (* wraps *) let (bit[20]) a_mid = a[(E + 19)..E] in - let (int) correction = a_top_correction(a_mid, R, B) in + let correction = a_top_correction(a_mid, R, B) in let a_top = a[63..(E+20)] in - let (bit[64]) base = EXTZ((a_top + correction) : B) in - base << E + let (bit[64]) base = EXTZ((a_top + correction) : B) << E in + unsigned(base) -function bit[65] getCapTop((CapStruct) c) = - let ([|63|]) E = unsigned(c.E) in - let (bool) s = c.sealed in +function CapLen getCapTop ((CapStruct) c) = + let ([|45|]) E = min(unsigned(c.E), 45) in let (bit[20]) B = c.B in let (bit[20]) T = c.T in let (bit[64]) a = c.address in - let (bit[20]) R = B - 0x00100 in (* wraps *) + let (bit[20]) R = B - 0x01000 in (* wraps *) let (bit[20]) a_mid = a[(E + 19)..E] in - let (int) correction = a_top_correction(a_mid, R, T) in + let correction = a_top_correction(a_mid, R, T) in let a_top = a[63..(E+20)] in let (bit[65]) top1 = EXTZ((a_top + correction) : T) in - top1 << E + (CapLen) (top1 << E) -function bit[64] getCapOffset((CapStruct) c) = +function uint64 getCapOffset((CapStruct) c) = let base = getCapBase(c) in - c.address - base + unsigned(c.address) - base -function bit[65] getCapLength((CapStruct) c) = getCapTop(c) - (0b0 : getCapBase(c)) +function CapLen getCapLength((CapStruct) c) = getCapTop(c) - getCapBase(c) -function nat getCapCursor((CapStruct) cap) = unsigned(cap.address) +function uint64 getCapCursor((CapStruct) cap) = unsigned(cap.address) function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = let oldBase = getCapBase(c) in let oldTop = getCapTop(c) in - let (bit[64]) newAddress = oldBase + offset in + let (bit[64]) newAddress = oldBase + offset in let newCap = { c with address = newAddress } in let newBase = getCapBase(newCap) in let newTop = getCapTop(newCap) in @@ -251,20 +249,29 @@ function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = { if break then Some(result) else None; }} -function (bit[6]) computeE ((bit[65]) rlength) = +(* hw rounds up E to multiple of 4 *) +function [|48|] roundUp(([|45|]) e) = + let r = e mod 4 in + if (r == 0) + then e + else (e - r + 4) + + +function [|48|] computeE ((bit[65]) rlength) = let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in switch (msb) { - case (Some(b)) -> (bit[6]) b (* hw rounds up to multiple of 4 *) + (* above will always return <= 45 because 19 bits of zero are shifted in from right *) + case (Some(b)) -> {assert(b <= 45, None); roundUp (min(b,45)) } case None -> 0 - } + } function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) = (* {cap with base=base; length=(bit[64]) length; offset=0} *) - let (bit[6]) e = computeE(top - (0b0 : base)) in + let ([|48|]) e = computeE(top - (0b0 : base)) in let (bit[20]) B = base[(19+e)..e] in let (bit[20]) T = top[(19+e)..e] in let (bit[20]) T2 = T + if (top[(e - 1)..0] == 0) then 0 else 1 in - let newCap = {cap with E=e; B=B; T=T2} in + let newCap = {cap with E=(bit[6]) e; B=B; T=T2} in let newBase = getCapBase(newCap) in let newTop = getCapTop(newCap) in let exact = (base == newBase) & (top == newTop) in diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index 8cb162f8..388d9ed7 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) @@ -183,12 +183,12 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) = (true, {cap with sealed=true; otype=otype}) -function bit[64] getCapBase((CapStruct) c) = c.base -function bit[65] getCapTop((CapStruct) c) = (0b0 : c.base) + (0b0 : c.length) -function bit[64] getCapOffset((CapStruct) c) = c.offset -function bit[65] getCapLength((CapStruct) c) = EXTZ(c.length) +function uint64 getCapBase((CapStruct) c) = unsigned(c.base) +function CapLen getCapTop((CapStruct) c) = unsigned(c.base) + unsigned(c.length) +function uint64 getCapOffset((CapStruct) c) = unsigned(c.offset) +function CapLen getCapLength((CapStruct) c) = unsigned(c.length) -function nat getCapCursor((CapStruct) cap) = +function uint64 getCapCursor((CapStruct) cap) = (unsigned(cap.base) + unsigned(cap.offset)) mod (2 ** 64) function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index 7530c9cc..e1356ceb 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) @@ -83,21 +83,6 @@ function (CapStruct) readCapReg((regno) n) = function unit writeCapReg((regno) n, (CapStruct) cap) = CapRegs[n] := capStructToCapReg(cap) -(* -function (CapStruct) readCapReg((regno) n) = -function (CapReg) capStructToCapReg((CapStruct) cap) = -function (CapReg) memBitsToCapBits((bool) tag, (bit[8*cap_size_t]) b)function unit writeCapReg((regno) n, (CapStruct) cap) = -function bit[64] getCapBase((CapStruct) c) -function bit[65] getCapTop((CapStruct) c) -function bit[64] getCapOffset((CapStruct) c) -function bit[65] getCapLength((CapStruct) c) = getCapTop(c) - (0b0 : getCapBase(c)) -function nat getCapCursor((CapStruct) cap) -function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) -function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) -function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) -function CapStruct int_to_cap ((bit[64]) offset) -*) - typedef CapEx = enumerate { CapEx_None; CapEx_LengthViolation; @@ -171,14 +156,19 @@ register CapCauseReg CapCause function forall Type 'o . 'o SignalException ((Exception) ex) = { + let pc = (bit[64]) PC in (* XXX Cast forces read of register. Sail bug? *) let pcc = capRegToCapStruct(PCC) in - let (success, epcc) = setCapOffset(pcc, PC) in - C31 := capStructToCapReg(epcc); + let (success, epcc) = setCapOffset(pcc, pc) in + if (success) then + C31 := capStructToCapReg(epcc) + else + C31 := capStructToCapReg(int_to_cap(getCapBase(pcc) + pc)); (* XXX what if not success? *) nextPCC := C29; (* KCC *) delayedPCC := C29; (* always write delayedPCC together whether PCC so that non-capability branches don't override PCC *) - SignalExceptionMIPS(ex, getCapBase(capRegToCapStruct(C29))); + let base = (bit[64]) (getCapBase(capRegToCapStruct(C29))) in + SignalExceptionMIPS(ex, base); } function unit ERETHook() = @@ -307,8 +297,8 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy cursor := getCapCursor(cap); vAddr := cursor + unsigned(addr); size := wordWidthBytes(width); - base := unsigned(getCapBase(cap)); - top := unsigned(getCapTop(cap)); + base := getCapBase(cap); + top := getCapTop(cap); if ((vAddr + size) > top) then (raise_c2_exception(CapEx_LengthViolation, capno)) else if (vAddr < (base)) then @@ -320,8 +310,8 @@ function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordTy function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = { incrementCP0Count(); let pcc = capRegToCapStruct(PCC) in - let base = unsigned(getCapBase(pcc)) in - let top = unsigned(getCapTop(pcc)) in + let base = getCapBase(pcc) in + let top = getCapTop(pcc) in let absPC = base + unsigned(vAddr) in if ((absPC mod 4) != 0) then (* bad PC alignment *) (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *) diff --git a/cheri/cheri_types.sail b/cheri/cheri_types.sail new file mode 100644 index 00000000..53d05cb5 --- /dev/null +++ b/cheri/cheri_types.sail @@ -0,0 +1,38 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +let (nat) max_otype = 0xffffff +let have_cp2 = true +typedef CapLen = [|0 : 2**65|] + diff --git a/etc/arm_header b/etc/arm_header index 566020aa..28639935 100644 --- a/etc/arm_header +++ b/etc/arm_header @@ -1,6 +1,6 @@ -Copyright (c) 2015-2016 Shaked Flur -Copyright (c) 2015-2016 Kathyrn Gray +Copyright (c) 2015-2017 Shaked Flur +Copyright (c) 2015-2017 Kathyrn Gray All rights reserved. This software was developed by the University of Cambridge Computer diff --git a/etc/headache_config b/etc/headache_config index a9d518f1..e8745fee 100644 --- a/etc/headache_config +++ b/etc/headache_config @@ -1,2 +1,3 @@ - ".*\\.lem" -> frame open:"(*" line:"=" close:"*)" -| ".*\\.sail" -> frame open:"(*" line:"=" close:"*)" + ".*\\.mllib" -> frame open:"(*" line:"=" close:"*)" +| ".*\\.lem" -> frame open:"(*" line:"=" close:"*)" +| ".*\\.sail" -> frame open:"(*" line:"=" close:"*)" diff --git a/etc/mips_header b/etc/mips_header index baf682e8..4a99ad2e 100644 --- a/etc/mips_header +++ b/etc/mips_header @@ -1,6 +1,6 @@ -Copyright (c) 2015-2016 Robert M. Norton -Copyright (c) 2015-2016 Kathyrn Gray +Copyright (c) 2015-2017 Robert M. Norton +Copyright (c) 2015-2017 Kathyrn Gray All rights reserved. This software was developed by the University of Cambridge Computer diff --git a/language/Makefile b/language/Makefile index 0c7563ce..1420ab1f 100644 --- a/language/Makefile +++ b/language/Makefile @@ -1,6 +1,6 @@ #OTT=../../../rsem/ott/bin/ott # this is the binary that gets rebuilt by make in ott/src: -OTT=../../../rsem/ott/src/ott +OTT=../../../github/ott/src/ott OTTLIB=$(dir $(shell which ott))../hol .PHONY: all @@ -37,5 +37,6 @@ l2.lem: l2.ott l2_typ.ott clean: rm -rf *~ -rm -rf *.uo *.ui *.sig *.sml .HOLMK - -rm -f *.tex *.aux *.log *.dvi *.ps *.pdf + -rm -f *.aux *.log *.dvi *.ps *.pdf rm -rf l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem + rm -rf l2.tex doc_in.tex
\ No newline at end of file diff --git a/language/l2.ott b/language/l2.ott index efed02bd..c3807f6a 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -122,7 +122,7 @@ id :: '' ::= | atom :: M :: atom {{ ichlo (Id "atom") }} | vector :: M :: vector {{ ichlo (Id "vector") }} | list :: M :: list {{ ichlo (Id "list") }} - | set :: M :: set {{ ichlo (Id "set") }} +% | set :: M :: set {{ ichlo (Id "set") }} | reg :: M :: reg {{ ichlo (Id "reg") }} | to_num :: M :: tonum {{ com Built in function identifiers }} {{ ichlo (Id "to_num") }} | to_vec :: M :: tovec {{ ichlo (Id "to_vec") }} @@ -135,7 +135,7 @@ id :: '' ::= % targets use alphabetical infix operators. kid :: '' ::= - {{ com variables with kind, ticked to differntiate from program variables }} + {{ com variables with kind, ticked to differentiate from program variables }} {{ aux _ l }} | ' x :: :: var @@ -687,7 +687,7 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} - | id ( exp1 , .. , expn ) :: :: memory {{ com memory write via function call }} + | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} | ( typ ) id :: :: cast | ( lexp0 , .. , lexpn ) :: :: tup {{ com set multiple at a time, a check will ensure it's not memory }} @@ -708,7 +708,7 @@ fexps :: 'FES_' ::= | fexp1 ; ... ; fexpn semi_opt :: :: Fexps opt_default :: 'Def_val_' ::= - {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }} + {{ com Optional default value for indexed vectors, to define a default value for any unspecified positions in a sparse map }} {{ aux _ annot }} {{ auxparam 'a }} | :: :: empty | ; default = exp :: :: dec diff --git a/language/manual.pdf b/language/manual.pdf Binary files differdeleted file mode 100644 index d848b8da..00000000 --- a/language/manual.pdf +++ /dev/null diff --git a/language/manual.tex b/language/manual.tex index 86aaa8b0..5d4b9d6a 100644 --- a/language/manual.tex +++ b/language/manual.tex @@ -17,101 +17,6 @@ \newpage -\section{Introduction} - -This is a manual describing the Sail specification language, its -common library, compiler, interpreter and type system. However it is -currently in early stages of being written, so questions to the -developers are highly encouraged. - -\section{Tips for Writing Sail specifications} - -This section attempts to offer advice for writing Sail specifications -that will work well with the Sail executable interpreter and -compilers. - -These tips use ideomatic Sail code; the Sail syntax is formally -defined in following section. - -Some tips might also be advice for good ways to specify instructions; -this will come from a combination of users and Sail developers. - -\begin{itemize} - -\item Declare memory access functions as one read, one write announce, - and one write value for each kind of access. - -For basic user-mode instructions, there should be the need for only -one memory read and two memory write function. These should each be -declared using {\tt val extern} and should have effect {\tt wmem} and -{\tt rmem} accordingly. - -Commonly, a memory read function will take as parameters a size (an -number below 32) and an address and return a bit vector with length (8 -* size). The sequential and concurrent interpreters both only read and -write memory as a factor of bytes. - -\item Declare a default vector order - -Vectors can be either decreasing or increasing, i.e. if we have a -vector \emph{a} with elements [1,2,3] then in an increasing specification the 1 is accessed -with {\tt a[0]} but with {\tt a[2]} in a decreasing system. Early in -your specification, it is beneficial to clarity to say default Ord inc -or default Ord dec. - -\item Vectors don't necessarily begin indexing at 0 or n-1 - -Without any additional specification, a vector will begin indexing at -0 in an increasing spec and n-1 in a decreasing specification. A type -declaration can reset this first position to any number. - -Importantly, taking a slice of a vector does not reset the indexes. So -if {\tt a = [1,2,3,4]} in an increasing system the slice {\tt a[2 - ..3]} generates the vector {\tt [3,4]} and the 3 is indexed at 2 in either vector. - -\item Be precise in numeric types. - -While Sail includes very wide types like int and nat, consider that -for bounds checking, numeric operations, and and clear understanding, -these really are unbounded quantities. If you know that a number in -the specification will range only between 0 and 32, 0 and 4, $-32$ to -32, it is better to use a specific range type such as $[|32|]$. - -Similarly, if you don't know the range precisely, it may also be best -to remain polymorphic and let Sail's type resolution work out bounds -in a particular use rather than removing all bounds; to do this, use -[:'n:] to say that it will polymorphically take some number. - -\item Use bit vectors for registers. - -Sail the language will readily allow a register to store a value of -any type. However, the Sail executable interpreter expects that it is -simulating a uni-processor machine where all registers are bit -vectors. - -A vector of length one, such as \emph{a} can read the element of \emph{a} -either with {\tt a} or {\tt a[0]}. - -\item Have functions named decode and execute to evaluate - instructions. - -The sail interpreter is hard-wired to look for functions with these names. - -\item Type annotations are necessary to read the contents of a - register into a local variable. - -The code {\tt x := GPR[4]}, where GPR is a vector of general purpose -registers, will store a local reference to the fourth general purpose -register, not the contents of that registe, i.e. this will not read -the register. To read the register contents into a local variable, the -type is required explicitly so {\tt (bit[64]) x := GPR[4]} reads the -register contents into x. The type annotation may be on either side of -the assignment. - -\end{itemize} - - - \section{Sail syntax} \ottgrammartabular{ diff --git a/manual.pdf b/manual.pdf deleted file mode 120000 index ed8af31e..00000000 --- a/manual.pdf +++ /dev/null @@ -1 +0,0 @@ -language/manual.pdf
\ No newline at end of file diff --git a/mips/mips_epilogue.sail b/mips/mips_epilogue.sail index 3771e26e..50993949 100644 --- a/mips/mips_epilogue.sail +++ b/mips/mips_epilogue.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index 8b9ccd76..77ff6f2a 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 8975193c..d2a0fc6f 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) @@ -569,7 +569,7 @@ function bool isAddressAligned(addr, (WordType) wordType) = (4k) we don't need to worry about accesses spanning page boundaries either. *) -let alignment_width = 32 +let alignment_width = 16 function (bool) isAddressAligned (addr, (WordType) wordType) = let a = unsigned(addr) in ((a quot alignment_width) == (a + wordWidthBytes(wordType) - 1) quot alignment_width) diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail index 1a290ec7..36750583 100644 --- a/mips/mips_regfp.sail +++ b/mips/mips_regfp.sail @@ -1,3 +1,37 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + let (vector <0, 32, inc, string >) GPRs = [ "GPR00", "GPR01", "GPR02", "GPR03", "GPR04", "GPR05", "GPR06", "GPR07", "GPR08", "GPR09", "GPR10", "GPR11", "GPR12", "GPR13", "GPR14", "GPR15", "GPR16", "GPR17", "GPR18", "GPR19", "GPR20", diff --git a/mips/mips_ri.sail b/mips/mips_ri.sail index e1222b98..3f368111 100644 --- a/mips/mips_ri.sail +++ b/mips/mips_ri.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/mips/mips_tlb.sail b/mips/mips_tlb.sail index 98cabb4d..2e40deed 100644 --- a/mips/mips_tlb.sail +++ b/mips/mips_tlb.sail @@ -1,3 +1,36 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) = let entryValid = entry.valid in diff --git a/mips/mips_tlb_stub.sail b/mips/mips_tlb_stub.sail index 6c4ea057..a9970a4e 100644 --- a/mips/mips_tlb_stub.sail +++ b/mips/mips_tlb_stub.sail @@ -1,3 +1,37 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + function option<TLBIndexT> tlbSearch((bit[64]) VAddr) = None function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) = diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail index a620f5f3..357aa9dd 100644 --- a/mips/mips_wrappers.sail +++ b/mips/mips_wrappers.sail @@ -1,7 +1,7 @@ (*========================================================================*) (* *) -(* Copyright (c) 2015-2016 Robert M. Norton *) -(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* Copyright (c) 2015-2017 Robert M. Norton *) +(* Copyright (c) 2015-2017 Kathyrn Gray *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) diff --git a/src/LICENCE b/src/LICENCE new file mode 100644 index 00000000..5992fbfc --- /dev/null +++ b/src/LICENCE @@ -0,0 +1,39 @@ + Sail + +Copyright (c) 2013-2017 + Kathyrn Gray + Shaked Flur + Stephen Kell + Gabriel Kerneis + Robert Norton-Wright + Christopher Pulte + Peter Sewell + +All rights reserved. + +This software was developed by the University of Cambridge Computer +Laboratory as part of the Rigorous Engineering of Mainstream Systems +(REMS) project, funded by EPSRC grant EP/K008528/1. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. +2. Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + +THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR +CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF +USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND +ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT +OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +SUCH DAMAGE. diff --git a/src/Makefile b/src/Makefile index 7927f9bc..9b8b727d 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,3 +1,45 @@ +########################################################################## +# Sail # +# # +# Copyright (c) 2013-2017 # +# Kathyrn Gray # +# Shaked Flur # +# Stephen Kell # +# Gabriel Kerneis # +# Robert Norton-Wright # +# Christopher Pulte # +# Peter Sewell # +# # +# All rights reserved. # +# # +# This software was developed by the University of Cambridge Computer # +# Laboratory as part of the Rigorous Engineering of Mainstream Systems # +# (REMS) project, funded by EPSRC grant EP/K008528/1. # +# # +# Redistribution and use in source and binary forms, with or without # +# modification, are permitted provided that the following conditions # +# are met: # +# 1. Redistributions of source code must retain the above copyright # +# notice, this list of conditions and the following disclaimer. # +# 2. Redistributions in binary form must reproduce the above copyright # +# notice, this list of conditions and the following disclaimer in # +# the documentation and/or other materials provided with the # +# distribution. # +# # +# THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' # +# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED # +# TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A # +# PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR # +# CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, # +# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT # +# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF # +# USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND # +# ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, # +# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT # +# OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF # +# SUCH DAMAGE. # +########################################################################## + .PHONY: all sail test clean doc lib power test_power test_idempotence all: sail lib doc @@ -39,10 +81,10 @@ MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(BITBUCKET_ROOT)/sail/etc/regfp.sail CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri -CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail elf: make -C $(ELFDIR) diff --git a/src/Makefile-non-opam b/src/Makefile-non-opam index 11f510fe..18fe6aa4 100644 --- a/src/Makefile-non-opam +++ b/src/Makefile-non-opam @@ -1,3 +1,45 @@ +########################################################################## +# Sail # +# # +# Copyright (c) 2013-2017 # +# Kathyrn Gray # +# Shaked Flur # +# Stephen Kell # +# Gabriel Kerneis # +# Robert Norton-Wright # +# Christopher Pulte # +# Peter Sewell # +# # +# All rights reserved. # +# # +# This software was developed by the University of Cambridge Computer # +# Laboratory as part of the Rigorous Engineering of Mainstream Systems # +# (REMS) project, funded by EPSRC grant EP/K008528/1. # +# # +# Redistribution and use in source and binary forms, with or without # +# modification, are permitted provided that the following conditions # +# are met: # +# 1. Redistributions of source code must retain the above copyright # +# notice, this list of conditions and the following disclaimer. # +# 2. Redistributions in binary form must reproduce the above copyright # +# notice, this list of conditions and the following disclaimer in # +# the documentation and/or other materials provided with the # +# distribution. # +# # +# THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' # +# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED # +# TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A # +# PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR # +# CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, # +# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT # +# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF # +# USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND # +# ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, # +# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT # +# OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF # +# SUCH DAMAGE. # +########################################################################## + THIS_MAKEFILE := $(lastword $(MAKEFILE_LIST)) # NOTE: it matters that this path is *not* canonicalised (realpath'd). # If we realpath it, the ocaml deps files will include realpaths, and diff --git a/src/ast.ml b/src/ast.ml index 8bf3b60c..5eb45554 120000..100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -1 +1,581 @@ -../language/l2.ml
\ No newline at end of file +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +(* generated by Ott 0.25 from: l2.ott *) + + +type text = string + +type l = Parse_ast.l + +type 'a annot = l * 'a + + +type x = text (* identifier *) +type ix = text (* infix identifier *) + +type +base_kind_aux = (* base kind *) + BK_type (* kind of types *) + | BK_nat (* kind of natural number size expressions *) + | BK_order (* kind of vector order specifications *) + | BK_effect (* kind of effect sets *) + + +type +base_kind = + BK_aux of base_kind_aux * l + + +type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type +kid_aux = (* variables with kind, ticked to differntiate from program variables *) + Var of x + + +type +kind_aux = (* kinds *) + K_kind of (base_kind) list + + +type +id = + Id_aux of id_aux * l + + +type +kid = + Kid_aux of kid_aux * l + + +type +kind = + K_aux of kind_aux * l + + +type +nexp_aux = (* expression of kind Nat, for vector sizes and origins *) + Nexp_id of id (* identifier, bound by def Nat x = nexp *) + | Nexp_var of kid (* variable *) + | Nexp_constant of int (* constant *) + | Nexp_times of nexp * nexp (* product *) + | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction *) + | Nexp_exp of nexp (* exponential *) + | Nexp_neg of nexp (* For internal use *) + +and nexp = + Nexp_aux of nexp_aux * l + + +type +base_effect_aux = (* effect *) + BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_eamem (* signal effective address for writing memory *) + | BE_wmv (* write memory, sending only value *) + | BE_barr (* memory barrier *) + | BE_depend (* dynamic footprint *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) + | BE_escape (* Tracking of expressions and functions that might call exit *) + | BE_lset (* Local mutation happend; not user-writable *) + | BE_lret (* Local return happened; not user-writable *) + + +type +base_effect = + BE_aux of base_effect_aux * l + + +type +order_aux = (* vector order specifications, of kind Order *) + Ord_var of kid (* variable *) + | Ord_inc (* increasing (little-endian) *) + | Ord_dec (* decreasing (big-endian) *) + + +type +effect_aux = (* effect set, of kind Effects *) + Effect_var of kid + | Effect_set of (base_effect) list (* effect set *) + + +type +order = + Ord_aux of order_aux * l + + +type +effect = + Effect_aux of effect_aux * l + + +type +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) + + +type +n_constraint_aux = (* constraint over kind $_$ *) + NC_fixed of nexp * nexp + | NC_bounded_ge of nexp * nexp + | NC_bounded_le of nexp * nexp + | NC_nat_set_bounded of kid * (int) list + + +type +kinded_id = + KOpt_aux of kinded_id_aux * l + + +type +n_constraint = + NC_aux of n_constraint_aux * l + + +type +quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) + QI_id of kinded_id (* An optionally kinded identifier *) + | QI_const of n_constraint (* A constraint for this type *) + + +type +quant_item = + QI_aux of quant_item_aux * l + + +type +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of (quant_item) list + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + +type +lit_aux = (* Literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | L_num of int (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* constant representing undefined values *) + | L_string of string (* string constant *) + + +type +typquant = + TypQ_aux of typquant_aux * l + + +type +typ_aux = (* Type expressions, of kind $_$ *) + Typ_wild (* Unspecified type *) + | Typ_id of id (* Defined type *) + | Typ_var of kid (* Type variable *) + | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) + | Typ_tup of (typ) list (* Tuple type *) + | Typ_app of id * (typ_arg) list (* type constructor application *) + +and typ = + Typ_aux of typ_aux * l + +and typ_arg_aux = (* Type constructor arguments of all kinds *) + Typ_arg_nexp of nexp + | Typ_arg_typ of typ + | Typ_arg_order of order + | Typ_arg_effect of effect + +and typ_arg = + Typ_arg_aux of typ_arg_aux * l + + +type +lit = + L_aux of lit_aux * l + + +type +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ + + +type +'a pat_aux = (* Pattern *) + P_lit of lit (* literal constant pattern *) + | P_wild (* wildcard *) + | P_as of 'a pat * id (* named pattern *) + | P_typ of typ * 'a pat (* typed pattern *) + | P_id of id (* identifier *) + | P_app of id * ('a pat) list (* union constructor pattern *) + | P_record of ('a fpat) list * bool (* struct pattern *) + | P_vector of ('a pat) list (* vector pattern *) + | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *) + | P_vector_concat of ('a pat) list (* concatenated vector pattern *) + | P_tup of ('a pat) list (* tuple pattern *) + | P_list of ('a pat) list (* list pattern *) + +and 'a pat = + P_aux of 'a pat_aux * 'a annot + +and 'a fpat_aux = (* Field pattern *) + FP_Fpat of id * 'a pat + +and 'a fpat = + FP_aux of 'a fpat_aux * 'a annot + + +type +typschm = + TypSchm_aux of typschm_aux * l + + +type +'a reg_id_aux = + RI_id of id + + +type +'a exp_aux = (* Expression *) + E_block of ('a exp) list (* block *) + | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_cast of typ * 'a exp (* cast *) + | E_app of id * ('a exp) list (* function application *) + | E_app_infix of 'a exp * id * 'a exp (* infix function application *) + | E_tuple of ('a exp) list (* tuple *) + | E_if of 'a exp * 'a exp * 'a exp (* conditional *) + | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *) + | E_vector of ('a exp) list (* vector (indexed from 0) *) + | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *) + | E_vector_access of 'a exp * 'a exp (* vector access *) + | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *) + | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *) + | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *) + | E_vector_append of 'a exp * 'a exp (* vector concatenation *) + | E_list of ('a exp) list (* list *) + | E_cons of 'a exp * 'a exp (* cons *) + | E_record of 'a fexps (* struct *) + | E_record_update of 'a exp * 'a fexps (* functional update of struct *) + | E_field of 'a exp * id (* field projection from struct *) + | E_case of 'a exp * ('a pexp) list (* pattern matching *) + | E_let of 'a letbind * 'a exp (* let expression *) + | E_assign of 'a lexp * 'a exp (* imperative assignment *) + | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) + | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) + | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) + | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) + | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) + | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) + | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *) + | E_internal_exp_user of 'a annot * 'a annot (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_comment of string (* For generated unstructured comments *) + | E_comment_struc of 'a exp (* For generated structured comments *) + | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) + | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) + | E_internal_return of 'a exp (* For internal use to embed into monad definition *) + +and 'a exp = + E_aux of 'a exp_aux * 'a annot + +and 'a lexp_aux = (* lvalue expression *) + LEXP_id of id (* identifier *) + | LEXP_memory of id * ('a exp) list (* memory write via function call *) + | LEXP_cast of typ * id + | LEXP_tup of ('a lexp) list (* set multiple at a time, a check will ensure it's not memory *) + | LEXP_vector of 'a lexp * 'a exp (* vector element *) + | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) + | LEXP_field of 'a lexp * id (* struct field *) + +and 'a lexp = + LEXP_aux of 'a lexp_aux * 'a annot + +and 'a fexp_aux = (* Field-expression *) + FE_Fexp of id * 'a exp + +and 'a fexp = + FE_aux of 'a fexp_aux * 'a annot + +and 'a fexps_aux = (* Field-expression list *) + FES_Fexps of ('a fexp) list * bool + +and 'a fexps = + FES_aux of 'a fexps_aux * 'a annot + +and 'a opt_default_aux = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) + Def_val_empty + | Def_val_dec of 'a exp + +and 'a opt_default = + Def_val_aux of 'a opt_default_aux * 'a annot + +and 'a pexp_aux = (* Pattern match *) + Pat_exp of 'a pat * 'a exp + +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a annot + +and 'a letbind_aux = (* Let binding *) + LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *) + | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *) + +and 'a letbind = + LB_aux of 'a letbind_aux * 'a annot + + +type +'a reg_id = + RI_aux of 'a reg_id_aux * 'a annot + + +type +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of typ * id + + +type +name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string + + +type +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect + + +type +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp + + +type +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +type +tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_some of typquant * typ + + +type +'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) + AL_subreg of 'a reg_id * id + | AL_bit of 'a reg_id * 'a exp + | AL_slice of 'a reg_id * 'a exp * 'a exp + | AL_concat of 'a reg_id * 'a reg_id + + +type +type_union = + Tu_aux of type_union_aux * l + + +type +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of int (* single index *) + | BF_range of int * int (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * l + + +type +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l + + +type +effect_opt = + Effect_opt_aux of effect_opt_aux * l + + +type +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot + + +type +rec_opt = + Rec_aux of rec_opt_aux * l + + +type +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l + + +type +'a alias_spec = + AL_aux of 'a alias_spec_aux * 'a annot + + +type +'a default_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * kid + | DT_order of order + | DT_typ of typschm * id + + +type +'a type_def_aux = (* Type definition body *) + TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) + + +type +'a val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) + + +type +'a kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *) + KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) + | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) + | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) + | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) + + +type +'a scattered_def_aux = (* Function and type union definitions that can be spread across + a file. Each one must end in $_$ *) + SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of 'a funcl (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) + + +type +'a fundef_aux = (* Function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list + + +type +'a dec_spec_aux = (* Register declarations *) + DEC_reg of typ * id + | DEC_alias of id * 'a alias_spec + | DEC_typ_alias of typ * id * 'a alias_spec + + +type +'a default_spec = + DT_aux of 'a default_spec_aux * l + + +type +'a type_def = + TD_aux of 'a type_def_aux * 'a annot + + +type +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot + + +type +'a kind_def = + KD_aux of 'a kind_def_aux * 'a annot + + +type +'a scattered_def = + SD_aux of 'a scattered_def_aux * 'a annot + + +type +'a fundef = + FD_aux of 'a fundef_aux * 'a annot + + +type +'a dec_spec = + DEC_aux of 'a dec_spec_aux * 'a annot + + +type +'a dec_comm = (* Top-level generated comments *) + DC_comm of string (* generated unstructured comment *) + | DC_comm_struct of 'a def (* generated structured comment *) + +and 'a def = (* Top-level definition *) + DEF_kind of 'a kind_def (* definition of named kind identifiers *) + | DEF_type of 'a type_def (* type definition *) + | DEF_fundef of 'a fundef (* function definition *) + | DEF_val of 'a letbind (* value definition *) + | DEF_spec of 'a val_spec (* top-level type constraint *) + | DEF_default of 'a default_spec (* default kind and type assumptions *) + | DEF_scattered of 'a scattered_def (* scattered function and type definition *) + | DEF_reg_dec of 'a dec_spec (* register declaration *) + | DEF_comm of 'a dec_comm (* generated comments *) + + +type +'a defs = (* Definition sequence *) + Defs of ('a def) list + + + diff --git a/src/finite_map.ml b/src/finite_map.ml index 78925e37..411048b6 100644 --- a/src/finite_map.ml +++ b/src/finite_map.ml @@ -1,4 +1,47 @@ (**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + + +(**************************************************************************) (* Lem *) (* *) (* Dominic Mulligan, University of Cambridge *) @@ -44,6 +87,7 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) + (** finite map library *) module type Fmap = sig diff --git a/src/initial_check.ml b/src/initial_check.ml index 5b813c04..82cc6b7c 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Type_internal open Ast diff --git a/src/initial_check.mli b/src/initial_check.mli index 14108e08..5e4b7e77 100644 --- a/src/initial_check.mli +++ b/src/initial_check.mli @@ -1,3 +1,44 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) open Ast open Type_internal diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml index 562d778e..b2781350 100644 --- a/src/initial_check_full_ast.ml +++ b/src/initial_check_full_ast.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Type_internal open Ast open Type_internal diff --git a/src/initial_check_full_ast.mli b/src/initial_check_full_ast.mli index 57346dcf..be612532 100644 --- a/src/initial_check_full_ast.mli +++ b/src/initial_check_full_ast.mli @@ -1,3 +1,44 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) open Ast open Type_internal diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem index 074f3bc4..e603bb58 100644 --- a/src/lem_interp/instruction_extractor.lem +++ b/src/lem_interp/instruction_extractor.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + open import Interp_ast open import Interp_utilities open import Pervasives diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 9072a3bd..543b7639 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + open import Pervasives import Map import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *) diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem index 37719b1b..64fb14b2 120000..100644 --- a/src/lem_interp/interp_ast.lem +++ b/src/lem_interp/interp_ast.lem @@ -1 +1,711 @@ -../../language/l2.lem
\ No newline at end of file +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +(* generated by Ott 0.25 from: l2_typ.ott l2.ott *) +open import Pervasives + +open import Map +open import Maybe +open import Set_extra + +type l = + | Unknown + | Int of string * maybe l (*internal types, functions*) + | Range of string * nat * nat * nat * nat + | Generated of l (*location for a generated node, where l is the location of the closest original source*) + +type annot 'a = l * 'a + +val duplicates : forall 'a. list 'a -> list 'a + +val set_from_list : forall 'a. list 'a -> set 'a + +val subst : forall 'a. list 'a -> list 'a -> bool + + +type x = string (* identifier *) +type ix = string (* infix identifier *) + +type base_kind_aux = (* base kind *) + | BK_type (* kind of types *) + | BK_nat (* kind of natural number size expressions *) + | BK_order (* kind of vector order specifications *) + | BK_effect (* kind of effect sets *) + + +type base_kind = + | BK_aux of base_kind_aux * l + + +type kid_aux = (* variables with kind, ticked to differntiate from program variables *) + | Var of x + + +type id_aux = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) + + +type kind_aux = (* kinds *) + | K_kind of list base_kind + + +type kid = + | Kid_aux of kid_aux * l + + +type id = + | Id_aux of id_aux * l + + +type kind = + | K_aux of kind_aux * l + + +type nexp_aux = (* expression of kind Nat, for vector sizes and origins *) + | Nexp_id of id (* identifier, bound by def Nat x = nexp *) + | Nexp_var of kid (* variable *) + | Nexp_constant of integer (* constant *) + | Nexp_times of nexp * nexp (* product *) + | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction *) + | Nexp_exp of nexp (* exponential *) + | Nexp_neg of nexp (* For internal use *) + +and nexp = + | Nexp_aux of nexp_aux * l + + +type base_effect_aux = (* effect *) + | BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_eamem (* signal effective address for writing memory *) + | BE_wmv (* write memory, sending only value *) + | BE_barr (* memory barrier *) + | BE_depend (* dynamic footprint *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) + | BE_escape (* Tracking of expressions and functions that might call exit *) + | BE_lset (* Local mutation happend; not user-writable *) + | BE_lret (* Local return happened; not user-writable *) + + +type base_effect = + | BE_aux of base_effect_aux * l + + +type order_aux = (* vector order specifications, of kind Order *) + | Ord_var of kid (* variable *) + | Ord_inc (* increasing (little-endian) *) + | Ord_dec (* decreasing (big-endian) *) + + +type effect_aux = (* effect set, of kind Effects *) + | Effect_var of kid + | Effect_set of list base_effect (* effect set *) + + +type order = + | Ord_aux of order_aux * l + + +type effect = + | Effect_aux of effect_aux * l + +let effect_union e1 e2 = + match (e1,e2) with + | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l + end + + +type kinded_id_aux = (* optionally kind-annotated identifier *) + | KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) + + +type n_constraint_aux = (* constraint over kind $Nat$ *) + | NC_fixed of nexp * nexp + | NC_bounded_ge of nexp * nexp + | NC_bounded_le of nexp * nexp + | NC_nat_set_bounded of kid * list integer + + +type kinded_id = + | KOpt_aux of kinded_id_aux * l + + +type n_constraint = + | NC_aux of n_constraint_aux * l + + +type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) + | QI_id of kinded_id (* An optionally kinded identifier *) + | QI_const of n_constraint (* A constraint for this type *) + + +type quant_item = + | QI_aux of quant_item_aux * l + + +type typquant_aux = (* type quantifiers and constraints *) + | TypQ_tq of list quant_item + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + +type lit_aux = (* Literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of integer (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* constant representing undefined values *) + | L_string of string (* string constant *) + + +type typquant = + | TypQ_aux of typquant_aux * l + + +type typ_aux = (* Type expressions, of kind $Type$ *) + | Typ_wild (* Unspecified type *) + | Typ_id of id (* Defined type *) + | Typ_var of kid (* Type variable *) + | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) + | Typ_tup of list typ (* Tuple type *) + | Typ_app of id * list typ_arg (* type constructor application *) + +and typ = + | Typ_aux of typ_aux * l + +and typ_arg_aux = (* Type constructor arguments of all kinds *) + | Typ_arg_nexp of nexp + | Typ_arg_typ of typ + | Typ_arg_order of order + | Typ_arg_effect of effect + +and typ_arg = + | Typ_arg_aux of typ_arg_aux * l + + +type lit = + | L_aux of lit_aux * l + + +type typschm_aux = (* type scheme *) + | TypSchm_ts of typquant * typ + + +type pat_aux 'a = (* Pattern *) + | P_lit of lit (* literal constant pattern *) + | P_wild (* wildcard *) + | P_as of (pat 'a) * id (* named pattern *) + | P_typ of typ * (pat 'a) (* typed pattern *) + | P_id of id (* identifier *) + | P_app of id * list (pat 'a) (* union constructor pattern *) + | P_record of list (fpat 'a) * bool (* struct pattern *) + | P_vector of list (pat 'a) (* vector pattern *) + | P_vector_indexed of list (integer * (pat 'a)) (* vector pattern (with explicit indices) *) + | P_vector_concat of list (pat 'a) (* concatenated vector pattern *) + | P_tup of list (pat 'a) (* tuple pattern *) + | P_list of list (pat 'a) (* list pattern *) + +and pat 'a = + | P_aux of (pat_aux 'a) * annot 'a + +and fpat_aux 'a = (* Field pattern *) + | FP_Fpat of id * (pat 'a) + +and fpat 'a = + | FP_aux of (fpat_aux 'a) * annot 'a + + +type typschm = + | TypSchm_aux of typschm_aux * l + + +type reg_id_aux 'a = + | RI_id of id + + +type exp_aux 'a = (* Expression *) + | E_block of list (exp 'a) (* block *) + | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_cast of typ * (exp 'a) (* cast *) + | E_app of id * list (exp 'a) (* function application *) + | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *) + | E_tuple of list (exp 'a) (* tuple *) + | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) + | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) + | E_vector of list (exp 'a) (* vector (indexed from 0) *) + | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) + | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) + | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) + | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) + | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *) + | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) + | E_list of list (exp 'a) (* list *) + | E_cons of (exp 'a) * (exp 'a) (* cons *) + | E_record of (fexps 'a) (* struct *) + | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *) + | E_field of (exp 'a) * id (* field projection from struct *) + | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) + | E_let of (letbind 'a) * (exp 'a) (* let expression *) + | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) + | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) + | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) + | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) + | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) + | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) + | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) + | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) + | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *) + | E_comment of string (* For generated unstructured comments *) + | E_comment_struc of (exp 'a) (* For generated structured comments *) + | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) + | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) + | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *) + +and exp 'a = + | E_aux of (exp_aux 'a) * annot 'a + +and lexp_aux 'a = (* lvalue expression *) + | LEXP_id of id (* identifier *) + | LEXP_memory of id * list (exp 'a) (* memory write via function call *) + | LEXP_cast of typ * id + | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *) + | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) + | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) + | LEXP_field of (lexp 'a) * id (* struct field *) + +and lexp 'a = + | LEXP_aux of (lexp_aux 'a) * annot 'a + +and fexp_aux 'a = (* Field-expression *) + | FE_Fexp of id * (exp 'a) + +and fexp 'a = + | FE_aux of (fexp_aux 'a) * annot 'a + +and fexps_aux 'a = (* Field-expression list *) + | FES_Fexps of list (fexp 'a) * bool + +and fexps 'a = + | FES_aux of (fexps_aux 'a) * annot 'a + +and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) + | Def_val_empty + | Def_val_dec of (exp 'a) + +and opt_default 'a = + | Def_val_aux of (opt_default_aux 'a) * annot 'a + +and pexp_aux 'a = (* Pattern match *) + | Pat_exp of (pat 'a) * (exp 'a) + +and pexp 'a = + | Pat_aux of (pexp_aux 'a) * annot 'a + +and letbind_aux 'a = (* Let binding *) + | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) + | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) + +and letbind 'a = + | LB_aux of (letbind_aux 'a) * annot 'a + + +type reg_id 'a = + | RI_aux of (reg_id_aux 'a) * annot 'a + + +type type_union_aux = (* Type union constructors *) + | Tu_id of id + | Tu_ty_id of typ * id + + +type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string + + +type effect_opt_aux = (* Optional effect annotation for functions *) + | Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect + + +type funcl_aux 'a = (* Function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) + + +type rec_opt_aux = (* Optional recursive annotation for functions *) + | Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +type tannot_opt_aux = (* Optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ + + +type alias_spec_aux 'a = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) + | AL_subreg of (reg_id 'a) * id + | AL_bit of (reg_id 'a) * (exp 'a) + | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) + | AL_concat of (reg_id 'a) * (reg_id 'a) + + +type type_union = + | Tu_aux of type_union_aux * l + + +type index_range_aux = (* index specification, for bitfields in register types *) + | BF_single of integer (* single index *) + | BF_range of integer * integer (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + | BF_aux of index_range_aux * l + + +type name_scm_opt = + | Name_sect_aux of name_scm_opt_aux * l + + +type effect_opt = + | Effect_opt_aux of effect_opt_aux * l + + +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * annot 'a + + +type rec_opt = + | Rec_aux of rec_opt_aux * l + + +type tannot_opt = + | Typ_annot_opt_aux of tannot_opt_aux * l + + +type alias_spec 'a = + | AL_aux of (alias_spec_aux 'a) * annot 'a + + +type default_spec_aux 'a = (* Default kinding or typing assumption *) + | DT_kind of base_kind * kid + | DT_order of order + | DT_typ of typschm * id + + +type type_def_aux 'a = (* Type definition body *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + + +type val_spec_aux 'a = (* Value type specification *) + | VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) + + +type kind_def_aux 'a = (* Definition body for elements of kind; many are shorthands for type\_defs *) + | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *) + | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) + | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | KD_enum of kind * id * name_scm_opt * list id * bool (* enumeration type definition *) + | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + + +type scattered_def_aux 'a = (* Function and type union definitions that can be spread across + a file. Each one must end in $id$ *) + | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) + + +type fundef_aux 'a = (* Function definition *) + | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) + + +type dec_spec_aux 'a = (* Register declarations *) + | DEC_reg of typ * id + | DEC_alias of id * (alias_spec 'a) + | DEC_typ_alias of typ * id * (alias_spec 'a) + + +type default_spec 'a = + | DT_aux of (default_spec_aux 'a) * l + + +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a + + +type val_spec 'a = + | VS_aux of (val_spec_aux 'a) * annot 'a + + +type kind_def 'a = + | KD_aux of (kind_def_aux 'a) * annot 'a + + +type scattered_def 'a = + | SD_aux of (scattered_def_aux 'a) * annot 'a + + +type fundef 'a = + | FD_aux of (fundef_aux 'a) * annot 'a + + +type dec_spec 'a = + | DEC_aux of (dec_spec_aux 'a) * annot 'a + + +type dec_comm 'a = (* Top-level generated comments *) + | DC_comm of string (* generated unstructured comment *) + | DC_comm_struct of (def 'a) (* generated structured comment *) + +and def 'a = (* Top-level definition *) + | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *) + | DEF_type of (type_def 'a) (* type definition *) + | DEF_fundef of (fundef 'a) (* function definition *) + | DEF_val of (letbind 'a) (* value definition *) + | DEF_spec of (val_spec 'a) (* top-level type constraint *) + | DEF_default of (default_spec 'a) (* default kind and type assumptions *) + | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *) + | DEF_reg_dec of (dec_spec 'a) (* register declaration *) + | DEF_comm of (dec_comm 'a) (* generated comments *) + + +type defs 'a = (* Definition sequence *) + | Defs of list (def 'a) + + +let rec remove_one i l = + match l with + | [] -> [] + | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) +end + +let rec remove_from l l2 = + match l2 with + | [] -> l + | i::l2' -> remove_from (remove_one i l) l2' +end + +let disjoint s1 s2 = Set.null (s1 inter s2) + +let rec disjoint_all sets = + match sets with + | [] -> true + | s1::[] -> true + | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) +end + + +type ne = (* internal numeric expressions *) + | Ne_id of x + | Ne_var of x + | Ne_const of integer + | Ne_inf + | Ne_mult of ne * ne + | Ne_add of list ne + | Ne_minus of ne * ne + | Ne_exp of ne + | Ne_unary of ne + + +type k = (* Internal kinds *) + | Ki_typ + | Ki_nat + | Ki_ord + | Ki_efct + | Ki_ctor of list k * k + | Ki_infer (* Representing an unknown kind, inferred by context *) + + +type nec = (* Numeric expression constraints *) + | Nec_lteq of ne * ne + | Nec_eq of ne * ne + | Nec_gteq of ne * ne + | Nec_in of x * list integer + | Nec_cond of list nec * list nec + | Nec_branch of list nec + + +type tid = (* A type identifier or type variable *) + | Tid_id of id + | Tid_var of kid + + +type kinf = (* Whether a kind is default or from a local binding *) + | Kinf_k of k + | Kinf_def of k + + +type t = (* Internal types *) + | T_id of x + | T_var of x + | T_fn of t * t * effect + | T_tup of list t + | T_app of x * t_args + | T_abbrev of t * t + +and t_arg = (* Argument to type constructors *) + | T_arg_typ of t + | T_arg_nexp of ne + | T_arg_effect of effect + | T_arg_order of order + +and t_args = (* Arguments to type constructors *) + | T_args of list t_arg + + +type tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) + | Tag_empty + | Tag_intro (* Denotes an assignment and lexp that introduces a binding *) + | Tag_set (* Denotes an expression that mutates a local variable *) + | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *) + | Tag_global (* Globally let-bound or enumeration based value/variable *) + | Tag_ctor (* Data constructor from a type union *) + | Tag_extern of maybe string (* External function, specied only with a val statement *) + | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) + | Tag_spec + | Tag_enum of integer + | Tag_alias + | Tag_unknown of maybe string (* Tag to distinguish an unknown path from a non-analysis non deterministic path *) + + +type tinf = (* Type variables, type, and constraints, bound to an identifier *) + | Tinf_typ of t + | Tinf_quant_typ of (map tid kinf) * list nec * tag * t + + +type conformsto = (* how much conformance does overloading need *) + | Conformsto_full + | Conformsto_parm + + +type widenvec = + | Widenvec_widen + | Widenvec_dont + | Widenvec_dontcare + + +type widennum = + | Widennum_widen + | Widennum_dont + | Widennum_dontcare + + +type tinflist = (* In place so that a list of tinfs can be referred to without the dot form *) + | Tinfs_empty + | Tinfs_ls of list tinf + + +type widening = (* Should we widen vector start locations, should we widen atoms and ranges *) + | Widening_w of widennum * widenvec + + type definition_env = + | DenvEmp + | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) + + +let blength (bit) = Ne_const 8 +let hlength (bit) = Ne_const 8 + + type env = + | EnvEmp + | Env of (map id tinf) * definition_env + + type inf = + | Iemp + | Inf of (list nec) * effect + + val denv_union : definition_env -> definition_env -> definition_env + let denv_union de1 de2 = + match (de1,de2) with + | (DenvEmp,de2) -> de2 + | (de1,DenvEmp) -> de1 + | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> + Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) + end + + val env_union : env -> env -> env + let env_union e1 e2 = + match (e1,e2) with + | (EnvEmp,e2) -> e2 + | (e1,EnvEmp) -> e1 + | ((Env te1 de1),(Env te2 de2)) -> + Env (te1 union te2) (denv_union de1 de2) + end + +let inf_union i1 i2 = + match (i1,i2) with + | (Iemp,i2) -> i2 + | (i1,Iemp) -> i1 + | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) + end + +let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) + + + +type E = env + + +type I = inf + + + diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 75e695eb..8c80b1c1 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + open import Interp_ast import Interp import Interp_lib @@ -1120,17 +1162,17 @@ let nias_of_instruction match (thread_ism, instruction_name) with | ("PPCGEN_ism", "B") -> let () = ensure (not unknown_nia_address) - "unexpected unknown/undefined address in nia_values" in + "unexpected unknown/undefined address in nia_values 1" in nias | ("PPCGEN_ism", "Bc") -> let () = ensure (not unknown_nia_address) - "unexpected unknown/undefined address in nia_values" in + "unexpected unknown/undefined address in nia_values 2" in NIA_successor :: nias | ("PPCGEN_ism", "Bclr") -> [ NIA_successor; NIA_LR ] | ("PPCGEN_ism", "Bcctr") -> [ NIA_successor; NIA_CTR ] | ("PPCGEN_ism", "Sc") -> let () = ensure (not unknown_nia_address) - "unexpected unknown/undefined address in nia_values" in + "unexpected unknown/undefined address in nia_values 3" in match instruction_fields with | [(_, _, lev)] -> (* LEV field is 7 bits long, pad it with false at beginning *) @@ -1175,13 +1217,49 @@ let nias_of_instruction | _ -> false end] + + (** hacky cut-and-paste for AArch64Gen, duplicating code just to see if this suffices *) + + | ("AArch64GenSail", "BranchImmediate") -> nias + | ("AArch64GenSail", "BranchConditional") -> NIA_successor :: nias + | ("AArch64GenSail", "CompareAndBranch") -> NIA_successor :: nias + | ("AArch64GenSail", "TestBitAndBranch") -> NIA_successor :: nias + + (* AArch64 calculated address branch *) + | ("AArch64GenSail", "branch_unconditional_register") -> + (* do some parsing of the ast fields to figure out which register holds + the branching address i.e. find n in "BR <Xn>". The ast constructor + from armV8.sail: (reg_index,BranchType) BranchRegister; *) + let n_integer = + match instruction_fields with + | [(_, _, n); _] -> integer_of_bit_list n + | _ -> fail + end + in + let () = ensure (0 <= n_integer && n_integer <= 31) + "expected register number from 0 to 31" + in + if n_integer = 31 then + nias (* BR XZR *) + else + (* look for Xn (which we actually call Rn) in regs_in *) + let n_reg = "R" ^ (String_extra.stringFromInteger n_integer) in + [NIA_register r | forall (r MEM regs_in) + | match r with + | (Reg name _ _ _) -> name = n_reg + | _ -> false + end] + + (** end of hacky *) + | ("AArch64LitmusSail", "CtrlDep") -> NIA_successor :: nias + | ("MIPS_ism", "B") -> fail - | _ -> + | (s1,s2) -> let () = ensure (not unknown_nia_address) - "unexpected unknown/undefined address in nia_values" in + ("unexpected unknown/undefined address in nia_values 4 (\""^s1^"\", \""^s2^"\")") in [ NIA_successor ] end diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 1de2de77..27165b15 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + (* PS NOTES FOR KATHY: pls also change: diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index 625dfb6c..36a31f3f 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + open import Pervasives open import Interp_utilities open import Interp @@ -701,15 +743,15 @@ let rec shift_op_vec op v = let fail () = Assert_extra.failwith ("shift_op_vec given unexpected " ^ (string_of_value v)) in let arith_op_help vl vr = match (vl,vr) with - | (V_vector b ord cs,V_lit (L_aux (L_num n) _)) -> - let n = natFromInteger n in - (match op with - | "<<" -> - V_vector b ord - ((from_n_to_n n ((length cs) - 1) cs) ++(List.replicate n (V_lit (L_aux L_zero Unknown)))) - | ">>" -> + | (V_vector b ord cs,V_lit (L_aux (L_num n) _)) -> + let n = natFromInteger n in + (match op with + | "<<" -> + V_vector b ord + ((from_n_to_n n ((length cs) - 1) cs) ++(List.replicate n (V_lit (L_aux L_zero Unknown)))) + | ">>" -> V_vector b ord - ((List.replicate n (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (n-1) cs)) + ((List.replicate n (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (((length cs) -1) - n) cs)) | "<<<" -> V_vector b ord ((from_n_to_n n ((length cs) -1) cs) ++ (from_n_to_n 0 (n-1) cs)) diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem index 63287a2e..86042d61 100644 --- a/src/lem_interp/interp_utilities.lem +++ b/src/lem_interp/interp_utilities.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + open import Interp_ast open import Pervasives open import Show_extra diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index 707ba9c3..7d182258 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + (* XXX this is copy-pasted from pretty_printer.ml with the following * changes: * - open Interp_ast instead of Ast; don't open Type_internals diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml index 202af6bb..88dbfbc8 100644 --- a/src/lem_interp/printing_functions.ml +++ b/src/lem_interp/printing_functions.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Printf ;; open Interp_ast ;; open Sail_impl_base ;; diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index a8291a78..6f5ca07a 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Printf ;; open Interp_ast ;; open Interp ;; diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml index cd038a7a..af9a1e0e 100644 --- a/src/lem_interp/run_interp_model.ml +++ b/src/lem_interp/run_interp_model.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Printf open Interp_ast open Sail_impl_base diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 81e6bd6e..813bef3a 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Printf ;; open Format ;; open Big_int ;; diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index 40a6495b..d58a6bd0 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Printf ;; open Format ;; open Big_int ;; diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 99a6e681..37685233 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Printf ;; open Format ;; open Big_int ;; @@ -623,7 +665,7 @@ let cheri_register_data_all = mips_register_data_all @ [ let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory = let initial_stack_data = [] in - let initial_cap_val_int = Nat_big_num.of_string "0x1fffe5a00000800000000000000000000" in (* hex((0x80000 << 64) + (45 << 105) + (0x7fff << 113) + (1 << 128)) *) + let initial_cap_val_int = Nat_big_num.of_string "0x1fffe0000000800000000000000000000" in (* hex((0x80000 << 64) + (0x7fff << 113) + (1 << 128)) *) let initial_cap_val_reg = Sail_impl_base.register_value_of_integer 129 128 D_decreasing initial_cap_val_int in let initial_register_abi_data : (string * Sail_impl_base.register_value) list = [ ("CP0Status", Sail_impl_base.register_value_of_integer 32 31 D_decreasing (Nat_big_num.of_string "0x00400000")); diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 3f38f521..97c7cff1 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + open import Pervasives_extra (* maybe isn't a member of type Ord - this should be in the Lem standard library*) diff --git a/src/lem_interp/type_check.lem b/src/lem_interp/type_check.lem index ec8e46bc..179e53d3 100644 --- a/src/lem_interp/type_check.lem +++ b/src/lem_interp/type_check.lem @@ -1,3 +1,45 @@ +(*========================================================================*) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + open import Pervasives import Map import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *) diff --git a/src/lexer.mll b/src/lexer.mll index c2b95004..98c9098d 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) { diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml index 2be63ad7..765553d3 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Ocamlbuild_plugin ;; open Command ;; open Pathname ;; diff --git a/src/parse_ast.ml b/src/parse_ast.ml index c4f970ec..2e72761e 120000..100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -1 +1,510 @@ -../language/l2_parse.ml
\ No newline at end of file +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +(* generated by Ott 0.25 from: l2_parse.ott *) + + +type text = string + +type l = + | Unknown + | Int of string * l option + | Generated of l + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + + +type x = text (* identifier *) +type ix = text (* infix identifier *) + +type +base_kind_aux = (* base kind *) + BK_type (* kind of types *) + | BK_nat (* kind of natural number size expressions *) + | BK_order (* kind of vector order specifications *) + | BK_effect (* kind of effect sets *) + + +type +base_kind = + BK_aux of base_kind_aux * l + + +type +base_effect_aux = (* effect *) + BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_wmv (* write memory value *) + | BE_eamem (* address for write signaled *) + | BE_barr (* memory barrier *) + | BE_depend (* dynmically dependent footprint *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) + | BE_escape + + +type +kid_aux = (* identifiers with kind, ticked to differntiate from program variables *) + Var of x + + +type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type +kind_aux = (* kinds *) + K_kind of (base_kind) list + + +type +base_effect = + BE_aux of base_effect_aux * l + + +type +kid = + Kid_aux of kid_aux * l + + +type +id = + Id_aux of id_aux * l + + +type +kind = + K_aux of kind_aux * l + + +type +atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) + ATyp_id of id (* identifier *) + | ATyp_var of kid (* ticked variable *) + | ATyp_constant of int (* constant *) + | ATyp_times of atyp * atyp (* product *) + | ATyp_sum of atyp * atyp (* sum *) + | ATyp_minus of atyp * atyp (* subtraction *) + | ATyp_exp of atyp (* exponential *) + | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *) + | ATyp_inc (* increasing (little-endian) *) + | ATyp_dec (* decreasing (big-endian) *) + | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) + | ATyp_set of (base_effect) list (* effect set *) + | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) + | ATyp_tup of (atyp) list (* Tuple type *) + | ATyp_app of id * (atyp) list (* type constructor application *) + +and atyp = + ATyp_aux of atyp_aux * l + + +type +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) + + +type +n_constraint_aux = (* constraint over kind $_$ *) + NC_fixed of atyp * atyp + | NC_bounded_ge of atyp * atyp + | NC_bounded_le of atyp * atyp + | NC_nat_set_bounded of kid * (int) list + + +type +kinded_id = + KOpt_aux of kinded_id_aux * l + + +type +n_constraint = + NC_aux of n_constraint_aux * l + + +type +quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) + QI_id of kinded_id (* An optionally kinded identifier *) + | QI_const of n_constraint (* A constraint for this type *) + + +type +quant_item = + QI_aux of quant_item_aux * l + + +type +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of (quant_item) list + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + +type +typquant = + TypQ_aux of typquant_aux * l + + +type +lit_aux = (* Literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | L_num of int (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* undefined value *) + | L_string of string (* string constant *) + + +type +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * atyp + + +type +lit = + L_aux of lit_aux * l + + +type +typschm = + TypSchm_aux of typschm_aux * l + + +type +pat_aux = (* Pattern *) + P_lit of lit (* literal constant pattern *) + | P_wild (* wildcard *) + | P_as of pat * id (* named pattern *) + | P_typ of atyp * pat (* typed pattern *) + | P_id of id (* identifier *) + | P_app of id * (pat) list (* union constructor pattern *) + | P_record of (fpat) list * bool (* struct pattern *) + | P_vector of (pat) list (* vector pattern *) + | P_vector_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *) + | P_vector_concat of (pat) list (* concatenated vector pattern *) + | P_tup of (pat) list (* tuple pattern *) + | P_list of (pat) list (* list pattern *) + +and pat = + P_aux of pat_aux * l + +and fpat_aux = (* Field pattern *) + FP_Fpat of id * pat + +and fpat = + FP_aux of fpat_aux * l + + +type +exp_aux = (* Expression *) + E_block of (exp) list (* block (parsing conflict with structs?) *) + | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) + | E_id of id (* identifier *) + | E_lit of lit (* literal constant *) + | E_cast of atyp * exp (* cast *) + | E_app of id * (exp) list (* function application *) + | E_app_infix of exp * id * exp (* infix function application *) + | E_tuple of (exp) list (* tuple *) + | E_if of exp * exp * exp (* conditional *) + | E_for of id * exp * exp * exp * atyp * exp (* loop *) + | E_vector of (exp) list (* vector (indexed from 0) *) + | E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *) + | E_vector_access of exp * exp (* vector access *) + | E_vector_subrange of exp * exp * exp (* subvector extraction *) + | E_vector_update of exp * exp * exp (* vector functional update *) + | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *) + | E_vector_append of exp * exp (* vector concatenation *) + | E_list of (exp) list (* list *) + | E_cons of exp * exp (* cons *) + | E_record of fexps (* struct *) + | E_record_update of exp * (exp) list (* functional update of struct *) + | E_field of exp * id (* field projection from struct *) + | E_case of exp * (pexp) list (* pattern matching *) + | E_let of letbind * exp (* let expression *) + | E_assign of exp * exp (* imperative assignment *) + | E_sizeof of atyp + | E_exit of exp + | E_return of exp + | E_assert of exp * exp + +and exp = + E_aux of exp_aux * l + +and fexp_aux = (* Field-expression *) + FE_Fexp of id * exp + +and fexp = + FE_aux of fexp_aux * l + +and fexps_aux = (* Field-expression list *) + FES_Fexps of (fexp) list * bool + +and fexps = + FES_aux of fexps_aux * l + +and opt_default_aux = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) + Def_val_empty + | Def_val_dec of exp + +and opt_default = + Def_val_aux of opt_default_aux * l + +and pexp_aux = (* Pattern match *) + Pat_exp of pat * exp + +and pexp = + Pat_aux of pexp_aux * l + +and letbind_aux = (* Let binding *) + LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *) + | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) + +and letbind = + LB_aux of letbind_aux * l + + +type +tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of typquant * atyp + + +type +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of atyp + + +type +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +type +funcl_aux = (* Function clause *) + FCL_Funcl of id * pat * exp + + +type +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of atyp * id + + +type +name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string + + +type +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l + + +type +effect_opt = + Effect_opt_aux of effect_opt_aux * l + + +type +rec_opt = + Rec_aux of rec_opt_aux * l + + +type +funcl = + FCL_aux of funcl_aux * l + + +type +type_union = + Tu_aux of type_union_aux * l + + +type +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of int (* single index *) + | BF_range of int * int (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * l + + +type +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l + + +type +default_typing_spec_aux = (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *) + DT_kind of base_kind * kid + | DT_order of base_kind * atyp + | DT_typ of typschm * id + + +type +fundef_aux = (* Function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list + + +type +type_def_aux = (* Type definition body *) + TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) + + +type +val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string + + +type +kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *) + KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) + | KD_record of kind * id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) + | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | KD_register of kind * id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) + + +type +dec_spec_aux = (* Register declarations *) + DEC_reg of atyp * id + | DEC_alias of id * exp + | DEC_typ_alias of atyp * id * exp + + +type +scattered_def_aux = (* Function and type union definitions that can be spread across + a file. Each one must end in $_$ *) + SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of funcl (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) + + +type +default_typing_spec = + DT_aux of default_typing_spec_aux * l + + +type +fundef = + FD_aux of fundef_aux * l + + +type +type_def = + TD_aux of type_def_aux * l + + +type +val_spec = + VS_aux of val_spec_aux * l + + +type +kind_def = + KD_aux of kind_def_aux * l + + +type +dec_spec = + DEC_aux of dec_spec_aux * l + + +type +scattered_def = + SD_aux of scattered_def_aux * l + + +type +def = (* Top-level definition *) + DEF_kind of kind_def (* definition of named kind identifiers *) + | DEF_type of type_def (* type definition *) + | DEF_fundef of fundef (* function definition *) + | DEF_val of letbind (* value definition *) + | DEF_spec of val_spec (* top-level type constraint *) + | DEF_default of default_typing_spec (* default kind and type assumptions *) + | DEF_scattered of scattered_def (* scattered definition *) + | DEF_reg_dec of dec_spec (* register declaration *) + + +type +lexp_aux = (* lvalue expression, can't occur out of the parser *) + LEXP_id of id (* identifier *) + | LEXP_mem of id * (exp) list + | LEXP_vector of lexp * exp (* vector element *) + | LEXP_vector_range of lexp * exp * exp (* subvector *) + | LEXP_field of lexp * id (* struct field *) + +and lexp = + LEXP_aux of lexp_aux * l + + +type +defs = (* Definition sequence *) + Defs of (def) list + + + diff --git a/src/parser.mly b/src/parser.mly index fb7ffa44..d172f61b 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1,47 +1,43 @@ /**************************************************************************/ -/* Lem */ +/* Sail */ /* */ -/* Dominic Mulligan, University of Cambridge */ -/* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt */ -/* Gabriel Kerneis, University of Cambridge */ -/* Kathy Gray, University of Cambridge */ -/* Peter Boehm, University of Cambridge (while working on Lem) */ -/* Peter Sewell, University of Cambridge */ -/* Scott Owens, University of Kent */ -/* Thomas Tuerk, University of Cambridge */ +/* Copyright (c) 2013-2017 */ +/* Kathyrn Gray */ +/* Shaked Flur */ +/* Stephen Kell */ +/* Gabriel Kerneis */ +/* Robert Norton-Wright */ +/* Christopher Pulte */ +/* Peter Sewell */ /* */ -/* The Lem sources are copyright 2010-2013 */ -/* by the UK authors above and Institut National de Recherche en */ -/* Informatique et en Automatique (INRIA). */ -/* */ -/* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} */ -/* are distributed under the license below. The former are distributed */ -/* under the LGPLv2, as in the LICENSE file. */ +/* All rights reserved. */ /* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ /* */ /* Redistribution and use in source and binary forms, with or without */ /* modification, are permitted provided that the following conditions */ /* are met: */ /* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ +/* notice, this list of conditions and the following disclaimer. */ /* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in the */ -/* documentation and/or other materials provided with the distribution. */ -/* 3. The names of the authors may not be used to endorse or promote */ -/* products derived from this software without specific prior written */ -/* permission. */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ /* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS */ -/* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED */ -/* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE */ -/* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY */ -/* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL */ -/* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE */ -/* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS */ -/* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER */ -/* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR */ -/* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN */ -/* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ /**************************************************************************/ %{ @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) (** pretty printing utilities *) @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) open Format diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll index e6534524..f648a594 100644 --- a/src/pre_lexer.mll +++ b/src/pre_lexer.mll @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) { diff --git a/src/pre_parser.mly b/src/pre_parser.mly index 85a6bf25..b595d55d 100644 --- a/src/pre_parser.mly +++ b/src/pre_parser.mly @@ -1,47 +1,43 @@ /**************************************************************************/ -/* Lem */ +/* Sail */ /* */ -/* Dominic Mulligan, University of Cambridge */ -/* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt */ -/* Gabriel Kerneis, University of Cambridge */ -/* Kathy Gray, University of Cambridge */ -/* Peter Boehm, University of Cambridge (while working on Lem) */ -/* Peter Sewell, University of Cambridge */ -/* Scott Owens, University of Kent */ -/* Thomas Tuerk, University of Cambridge */ +/* Copyright (c) 2013-2017 */ +/* Kathyrn Gray */ +/* Shaked Flur */ +/* Stephen Kell */ +/* Gabriel Kerneis */ +/* Robert Norton-Wright */ +/* Christopher Pulte */ +/* Peter Sewell */ /* */ -/* The Lem sources are copyright 2010-2013 */ -/* by the UK authors above and Institut National de Recherche en */ -/* Informatique et en Automatique (INRIA). */ -/* */ -/* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} */ -/* are distributed under the license below. The former are distributed */ -/* under the LGPLv2, as in the LICENSE file. */ +/* All rights reserved. */ /* */ +/* This software was developed by the University of Cambridge Computer */ +/* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ +/* (REMS) project, funded by EPSRC grant EP/K008528/1. */ /* */ /* Redistribution and use in source and binary forms, with or without */ /* modification, are permitted provided that the following conditions */ /* are met: */ /* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ +/* notice, this list of conditions and the following disclaimer. */ /* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in the */ -/* documentation and/or other materials provided with the distribution. */ -/* 3. The names of the authors may not be used to endorse or promote */ -/* products derived from this software without specific prior written */ -/* permission. */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ /* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS */ -/* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED */ -/* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE */ -/* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY */ -/* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL */ -/* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE */ -/* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS */ -/* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER */ -/* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR */ -/* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN */ -/* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ /**************************************************************************/ %{ diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 0da54e53..415d48fd 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Type_internal open Ast open Format @@ -246,38 +288,38 @@ let pp_format_lit_lem (L_aux(lit,l)) = let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l) -let rec pp_format_t t = +let rec pp_format_t_lem t = match t.t with | Tid i -> "(T_id \"" ^ i ^ "\")" | Tvar i -> "(T_var \"" ^ i ^ "\")" - | Tfn(t1,t2,_,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")" - | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])" - | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^ list_format "; " pp_format_targ args ^ "]))" - | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t ti) ^ " " ^ (pp_format_t ta) ^ ")" + | Tfn(t1,t2,_,e) -> "(T_fn " ^ (pp_format_t_lem t1) ^ " " ^ (pp_format_t_lem t2) ^ " " ^ pp_format_e_lem e ^ ")" + | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t_lem tups) ^ "])" + | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^ list_format "; " pp_format_targ_lem args ^ "]))" + | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t_lem ti) ^ " " ^ (pp_format_t_lem ta) ^ ")" | Tuvar(_) -> "(T_var \"fresh_v\")" | Toptions _ -> "(T_var \"fresh_v\")" -and pp_format_targ = function - | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")" - | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")" - | TA_eft e -> "(T_arg_effect " ^ pp_format_e e ^ ")" - | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")" -and pp_format_n n = +and pp_format_targ_lem = function + | TA_typ t -> "(T_arg_typ " ^ pp_format_t_lem t ^ ")" + | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n_lem n ^ ")" + | TA_eft e -> "(T_arg_effect " ^ pp_format_e_lem e ^ ")" + | TA_ord o -> "(T_arg_order " ^ pp_format_o_lem o ^ ")" +and pp_format_n_lem n = match n.nexp with | Nid (i, n) -> "(Ne_id \"" ^ i ^ " " ^ "\")" | Nvar i -> "(Ne_var \"" ^ i ^ "\")" | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")" | Npos_inf -> "Ne_inf" - | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])" - | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")" - | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")" - | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")" - | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")" - | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")" + | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n_lem n1) ^ "; " ^ (pp_format_n_lem n2) ^ "])" + | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")" + | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")" + | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")" + | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ ")" + | Nneg n -> "(Ne_unary " ^ (pp_format_n_lem n) ^ ")" | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")" | Nneg_inf -> "(Ne_unary Ne_inf)" | Npow _ -> "power_not_implemented" | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)" -and pp_format_e e = +and pp_format_e_lem e = "(Effect_aux " ^ (match e.effect with | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" @@ -285,7 +327,7 @@ and pp_format_e e = (list_format "; " pp_format_base_effect_lem es) ^ " ])" | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))") ^ " Unknown)" -and pp_format_o o = +and pp_format_o_lem o = "(Ord_aux " ^ (match o.order with | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" @@ -312,9 +354,9 @@ let rec pp_format_nes nes = "[" ^ (* (list_format "; " (fun ne -> match ne with - | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" - | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" - | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")" + | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" + | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" + | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])" | InS(_,_,ns) -> @@ -330,8 +372,8 @@ let pp_format_annot = function | NoTyp -> "Nothing" | Base((_,t),tag,nes,efct,efctsum,_) -> (*TODO print out bindings for use in pattern match in interpreter*) - "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ - pp_format_e efct ^ ", " ^ pp_format_e efctsum ^ "))" + "(Just (" ^ pp_format_t_lem t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ + pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))" | Overload _ -> "Nothing" let pp_annot ppf ant = base ppf (pp_format_annot ant) @@ -675,6 +717,116 @@ let pp_lem_defs ppf (Defs(defs)) = fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs + +(* ************************************************************************** + * pp from tannot to ASCII source, for pp of built-in type environment +*) + + + +let rec pp_format_t_ascii t = + match t.t with + | Tid i -> i + | Tvar i -> "'" ^ i + | Tfn(t1,t2,_,e) -> (pp_format_t_ascii t1) ^ " -> " ^ (pp_format_t_ascii t2) ^ " effect " ^ pp_format_e_ascii e + | Ttup(tups) -> "(" ^ (list_format ", " pp_format_t_ascii tups) ^ ")" + | Tapp(i,args) -> i ^ "<" ^ list_format ", " pp_format_targ_ascii args ^ ">" + | Tabbrev(ti,ta) -> (pp_format_t_ascii ti) (* (pp_format_t_ascii ta) *) + | Tuvar(_) -> failwith "Tuvar in pp_format_t_ascii" + | Toptions _ -> failwith "Toptions in pp_format_t_ascii" +and pp_format_targ_ascii = function + | TA_typ t -> pp_format_t_ascii t + | TA_nexp n -> pp_format_n_ascii n + | TA_eft e -> pp_format_e_ascii e + | TA_ord o -> pp_format_o_ascii o +and pp_format_n_ascii n = + match n.nexp with + | Nid (i, n) -> i (* from an abbreviation *) + | Nvar i -> "'" ^ i + | Nconst i -> (string_of_int (int_of_big_int i)) + | Npos_inf -> "infinity" + | Nadd(n1,n2) -> (pp_format_n_ascii n1) ^ "+" ^ (pp_format_n_ascii n2) + | Nsub(n1,n2) -> (pp_format_n_ascii n1) ^ "-" ^ (pp_format_n_ascii n2) + | Nmult(n1,n2) -> (pp_format_n_ascii n1) ^ "*" ^ (pp_format_n_ascii n2) + | N2n(n,_) -> "2**"^(pp_format_n_ascii n) (* string_of_big_int i ^ *) + | Nneg n -> "-" ^ (pp_format_n_ascii n) + | Nuvar _ -> failwith "Nuvar in pp_format_n_ascii" + | Nneg_inf -> "-infinity" + | Npow _ -> failwith "Npow in pp_format_n_ascii" + | Ninexact -> failwith "Ninexact in pp_format_n_ascii" +and pp_format_e_ascii e = + match e.effect with + | Evar i -> "'" ^ i + | Eset es -> "{" ^ + (list_format ", " pp_format_base_effect_ascii es) ^ "}" + | Euvar(_) -> failwith "Euvar in pp_format_e_ascii" +and pp_format_o_ascii o = + match o.order with + | Ovar i -> "'" ^ i + | Oinc -> "inc" + | Odec -> "dec" + | Ouvar(_) -> failwith "Ouvar in pp_format_o_ascii" +and pp_format_base_effect_ascii (BE_aux(e,l)) = + match e with + | BE_rreg -> "rreg" + | BE_wreg -> "wreg" + | BE_rmem -> "rmem" + | BE_wmem -> "wmem" + | BE_wmv -> "wmv" + | BE_eamem -> "eamem" + | BE_barr -> "barr" + | BE_depend -> "depend" + | BE_undef -> "undef" + | BE_unspec -> "unspec" + | BE_nondet -> "nondet" + | BE_lset -> "lset" + | BE_lret -> "lret" + | BE_escape -> "escape" + +and pp_format_nes_ascii nes = + list_format ", " pp_format_ne_ascii nes + +and pp_format_ne_ascii ne = + match ne with + | Lt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " < " ^ pp_format_n_ascii n2 + | LtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " <= " ^ pp_format_n_ascii n2 + | NtEq(_,n1,n2) -> pp_format_n_ascii n1 ^ " != " ^ pp_format_n_ascii n2 + | Eq(_,n1,n2) -> pp_format_n_ascii n1 ^ " = " ^ pp_format_n_ascii n2 + | GtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " >= " ^ pp_format_n_ascii n2 + | Gt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " > " ^ pp_format_n_ascii n2 + | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> + i ^ " IN {" ^ (list_format ", " string_of_int ns)^ "}" + | InS(_,_,ns) -> (* when the variable has been replaced by a unification variable, we use this *) + failwith "InS in pp_format_nes_ascii" (*"(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"*) + | Predicate(_,n1,n2) -> "flow_constraints(" ^ pp_format_ne_ascii n1 ^", "^ pp_format_ne_ascii n2 ^")" + | CondCons(_,_,_,nes_c,nes_t) -> + failwith "CondCons in pp_format_nes_ascii" (*"(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")"*) + | BranchCons(_,_,nes_b) -> + failwith "BranchCons in pp_format_nes_ascii" (*"(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"*) + + + +let rec pp_format_annot_ascii = function + | NoTyp -> "Nothing" + | Base((targs,t),tag,nes,efct,efctsum,_) -> + (*TODO print out bindings for use in pattern match in interpreter*) + "forall " ^ list_format ", " (function (i,k) -> kind_to_string k ^" "^ i) targs ^ + (match nes with [] -> "" | _ -> ", " ^ pp_format_nes_ascii nes) + ^ ". " + ^ pp_format_t_ascii t + +(* +^ " ********** " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ + pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))" +*) + | Overload (tannot, return_type_overloading_allowed, tannots) -> + pp_format_annot_ascii tannot ^ "\n" ^ String.concat "" (List.map (function tannot' -> " " ^ pp_format_annot_ascii tannot' ^ "\n") tannots) + + + + + + (**************************************************************************** * PPrint-based source-to-source pretty printer ****************************************************************************) diff --git a/src/pretty_print.mli b/src/pretty_print.mli index 500d19e2..9a002454 100644 --- a/src/pretty_print.mli +++ b/src/pretty_print.mli @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Ast open Type_internal @@ -11,3 +53,6 @@ val pp_lem_defs : Format.formatter -> tannot defs -> unit val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit + + +val pp_format_annot_ascii : tannot -> string diff --git a/src/process_file.ml b/src/process_file.ml index cda44e77..273979cf 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) open Type_internal diff --git a/src/process_file.mli b/src/process_file.mli index 66b1d8af..2c18b830 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) val parse_file : string -> Parse_ast.defs diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml index 0e2a2e17..5ff43208 100644 --- a/src/reporting_basic.ml +++ b/src/reporting_basic.ml @@ -1,4 +1,47 @@ (**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + + +(**************************************************************************) (* Lem *) (* *) (* Dominic Mulligan, University of Cambridge *) diff --git a/src/reporting_basic.mli b/src/reporting_basic.mli index 7362d44c..559be9d4 100644 --- a/src/reporting_basic.mli +++ b/src/reporting_basic.mli @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) (** Basic error reporting diff --git a/src/rewriter.ml b/src/rewriter.ml index 8582f3b5..dc96b952 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Big_int open Ast open Type_internal diff --git a/src/rewriter.mli b/src/rewriter.mli index d1d642ff..615d0fa0 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Big_int open Ast open Type_internal diff --git a/src/sail.ml b/src/sail.ml index 80560746..1230288b 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) open Process_file @@ -104,6 +100,18 @@ let main() = if !(opt_print_version) then Printf.printf "Sail private release \n" else + let ppd_initial_typ_env = + String.concat "" + (List.map + (function (id,tannot) -> + id ^ " : " ^ + Pretty_print.pp_format_annot_ascii tannot + ^ "\n") + (Type_internal.Envmap.to_list Type_internal.initial_typ_env)) in + Printf.printf "%s" ppd_initial_typ_env ; + + + let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in let ast = List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 4cfc1331..df2b6d61 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + (** A Sail library *) (* This library is not well-thought. It has grown driven by the need to diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index bddeb28c..8cb5a796 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Ast open Util open Big_int diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli index 068b3778..fa8dad3b 100644 --- a/src/spec_analysis.mli +++ b/src/spec_analysis.mli @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Ast open Util open Big_int diff --git a/src/test/mips/test_cp2_csetbounds_cases.elf b/src/test/mips/test_cp2_csetbounds_cases.elf Binary files differnew file mode 100755 index 00000000..9ba8ab94 --- /dev/null +++ b/src/test/mips/test_cp2_csetbounds_cases.elf diff --git a/src/type_check.ml b/src/type_check.ml index 63942df8..c4119281 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Big_int open Ast open Type_internal diff --git a/src/type_check.mli b/src/type_check.mli index 02fd2a80..4f78dd03 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Ast open Type_internal type kind = Type_internal.kind diff --git a/src/type_internal.ml b/src/type_internal.ml index 2770d827..b26a7ebd 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Ast open Util open Big_int @@ -200,7 +242,7 @@ type tannot = (*See .mli for purpose of attributes *) | Base of (t_params * t) * tag * nexp_range list * effect * effect * bounds_env (* First tannot is the most polymorphic version; the list includes all variants. All included t are Tfn *) - | Overload of tannot * bool * tannot list + | Overload of tannot * bool * tannot list (* these tannot's should all be Base *) type 'a emap = 'a Envmap.t @@ -1842,10 +1884,15 @@ let rec refine_requires check_nvar min_lt max_gt id cs = let nat_t = {t = Tapp("range",[TA_nexp n_zero;TA_nexp (mk_p_inf());])} let int_t = {t = Tapp("range",[TA_nexp (mk_n_inf());TA_nexp (mk_p_inf());])} -let uint8_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 8) (big_int_of_int 256))])} -let uint16_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 16) (big_int_of_int 65536))])} -let uint32_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 32) (big_int_of_string "4294967296"))])} -let uint64_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_2nc (mk_c_int 64) (big_int_of_string "18446744073709551616"))])} +let uint8_t = {t = Tapp("range",[TA_nexp n_zero; TA_nexp (mk_sub (mk_2nc (mk_c_int 8) (big_int_of_int 256)) n_one)])} +let uint16_t = {t = Tapp("range",[TA_nexp n_zero; + TA_nexp (mk_sub (mk_2nc (mk_c_int 16) (big_int_of_int 65536)) n_one)])} +let uint32_t = {t = Tapp("range",[TA_nexp n_zero; + TA_nexp (mk_sub (mk_2nc (mk_c_int 32) (big_int_of_string "4294967296")) n_one)])} +let uint64_t = {t = Tapp("range",[TA_nexp n_zero; + TA_nexp (mk_sub (mk_2nc (mk_c_int 64) (big_int_of_string "18446744073709551616")) + (mk_c_int 1)) + ])} let int8_t = {t = Tapp("range", [TA_nexp (mk_neg (mk_2nc (mk_c_int 7) (big_int_of_int 128))) ; TA_nexp (mk_c_int 127)])} @@ -1954,7 +2001,7 @@ let mk_bitwise_op name symb arity = (*lib_tannot (["n",{k=K_Nat};"o",{k=K_Ord}],mk_pure_fun svarg single_bit_vec_typ) (Some name) [];*) lib_tannot ([],mk_pure_fun barg bit_t) (Some (name ^ "_bit")) []])) -let initial_typ_env = +let initial_typ_env : tannot Envmap.t = Envmap.from_list [ ("ignore",lib_tannot ([("a",{k=K_Typ})],mk_pure_fun {t=Tvar "a"} unit_t) None []); ("Some", Base((["a",{k=K_Typ}], mk_pure_fun {t=Tvar "a"} {t=Tapp("option", [TA_typ {t=Tvar "a"}])}), @@ -2703,6 +2750,7 @@ let initial_typ_env = (mk_atom (mk_nv "o")))), External (Some "min"),[],pure_e,pure_e,nob)); ] + let rec typ_subst s_env leave_imp t = @@ -3350,6 +3398,12 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e (*let _ = Printf.eprintf "called type_coerce_internal is_explicit %b, widen %b, turning %s with actual %s into %s with actual %s\n" is_explicit widen (t_to_string t1) (t_to_string t1_actual) (t_to_string t2) (t_to_string t2_actual) in*) match t1_actual.t,t2_actual.t with + + (* Toptions is an internal constructor representing the type we're + going to be casting to and the natural type. source-language type + annotations might be demanding a coercion, so this checks + conformance and adds a coercion if needed *) + | Toptions(to1,Some to2),_ -> if (conforms_to_t d_env false true to1 t2_actual || conforms_to_t d_env false true to2 t2_actual) then begin t1_actual.t <- t2_actual.t; (t2,csp,pure_e,e) end @@ -3362,12 +3416,17 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | _,Toptions(to1,Some to2) -> if (conforms_to_t d_env false true to1 t1_actual || conforms_to_t d_env false true to2 t1_actual) then begin t2_actual.t <- t1_actual.t; (t1,csp,pure_e,e) end - else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^ + else eq_error l ((t_to_string t1) ^ " can match neither expected type " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2)) | _,Toptions(to1,None) -> if is_explicit then type_coerce_internal co d_env enforce is_explicit widen bounds t1_actual cs1 e to1 cs2 else (t1,csp,pure_e,e) + + (* recursive coercions to components of tuples. They may be + complex expressions, not top-level tuples, so we sometimes + need to add a pattern match. At present we do that almost + always, unnecessarily often. The any_coerced is wrong *) | Ttup t1s, Ttup t2s -> let tl1,tl2 = List.length t1s,List.length t2s in if tl1=tl2 then @@ -3396,10 +3455,16 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e (t2,csp@cs,efs,e') else eq_error l ("Found a tuple of length " ^ (string_of_int tl1) ^ " but expected a tuple of length " ^ (string_of_int tl2)) + + + (* all the Tapp cases *) | Tapp(id1,args1),Tapp(id2,args2) -> if id1=id2 && (id1 <> "vector") + (* no coercion needed, so fall back to consistency *) then let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e) else (match id1,id2,is_explicit with + + (* can coerce between two vectors just to change the start index *) | "vector","vector",_ -> (match args1,args2 with | [TA_nexp b1;TA_nexp r1;TA_ord o1;TA_typ t1i], @@ -3415,6 +3480,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e,pure_e,nob))),e),(l,tannot)) in (t2,cs@cs',pure_e,e') | _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded")) + + (* coercion from a bit vector into a number *) | "vector","range",_ -> (match args1,args2 with | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}], @@ -3429,6 +3496,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert non-bit vector into an range" | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) + + (* similar to vector/range case *) | "vector","atom",_ -> (match args1,args2 with | [TA_nexp b1;TA_nexp r1;TA_ord _;TA_typ {t=Tid "bit"}], @@ -3441,6 +3510,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert non-bit vector into an range" | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) + + (* coercion from number into bit vector, if there's an explicit type annotation in the source (the "true") *) + (* this can be lossy, if it doesn't fit into that vector, so we want to require the user to specify the vector size. It was desired by some users, but maybe should be turned back into an error and an explicit truncate function be used *) | "range","vector",true -> (match args2,args1 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], @@ -3464,6 +3536,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert a range into a non-bit vector" | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) + + (* similar to number to bit vector case *) | "atom","vector",true -> (match args2,args1 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], @@ -3486,6 +3560,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert a range into a non-bit vector" | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) + + (* implicit dereference of a register, from register<t> to t, and then perhaps also from t to the expected type *) | "register",_,_ -> (match args1 with | [TA_typ t] -> @@ -3501,16 +3577,24 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e let (t',cs,ef',e) = type_coerce co d_env Guarantee is_explicit widen bounds t new_e t2 in (t',cs,union_effects ef ef',e) | _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded")) + + (* otherwise in Tapp case, fall back on type_consistent *) | _,_,_ -> let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e)) + + (* bit vector of length 1 to bit *) | Tapp("vector",[TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") -> let cs = [Eq(co,r1,n_one)] in (t2,cs,pure_e,E_aux((E_app ((Id_aux (Id "most_significant", l)), [e])), (l, cons_tag_annot_efr t2 (External (Some "most_significant")) cs (get_cummulative_effects (get_eannot e))))) + + (* bit to a bitvector of length 1 *) | Tid("bit"),Tapp("vector",[TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) -> let cs = [Eq(co,r1,n_one)] in (t2,cs,pure_e,E_aux(E_vector [e], (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e))))) + + (* bit to a number range (including 0..1) *) | Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) -> let t',cs'= type_consistent co d_env enforce false {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} t2 in (t2,cs',pure_e, @@ -3521,6 +3605,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e E_aux(E_lit(L_aux(L_num 1,l)),(l,simple_annot t2))), (l,simple_annot t2));]), (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) + + + (* similar to above, bit to a singleton number range *) | Tid("bit"),Tapp("atom",[TA_nexp b1]) -> let t',cs'= type_consistent co d_env enforce false t2 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in (t2,cs',pure_e, @@ -3531,6 +3618,9 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e E_aux(E_lit(L_aux(L_num 1,l)),(l,simple_annot t2))), (l,simple_annot t2));]), (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) + + + (* number range to a bit *) | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid("bit") -> let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in let efr = get_cummulative_effects (get_eannot e) @@ -3539,6 +3629,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e E_aux(E_lit(L_aux(L_one,l)),(l,simple_annot bit_t)), E_aux(E_lit(L_aux(L_zero,l)),(l,simple_annot bit_t))), (l,simple_annot_efr bit_t efr))) + + (* similar to above *) | Tapp("atom",[TA_nexp b1]),Tid("bit") -> let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in let efr = get_cummulative_effects (get_eannot e) @@ -3546,6 +3638,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e E_aux(E_lit(L_aux(L_one,l)),(l,simple_annot bit_t)), E_aux(E_lit(L_aux(L_zero,l)),(l,simple_annot bit_t))), (l,simple_annot_efr bit_t efr))) + + (* number range to an enumeration type *) | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> (match Envmap.apply d_env.enum_env i with | Some(enums) -> @@ -3558,6 +3652,23 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e (l,simple_annot t2))) enums), (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))) + + (* similar to above *) + | Tapp("atom",[TA_nexp b1]),Tid(i) -> + (match Envmap.apply d_env.enum_env i with + | Some(enums) -> + let num_enums = List.length enums in + (t2,[GtEq(co,Require,b1,n_zero); + LtEq(co,Require,b1,mk_c(big_int_of_int num_enums))],pure_e, + E_aux(E_case(e, + List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),(l, simple_annot t1)), + E_aux(E_id(Id_aux(Id a,l)), + (l, tag_annot t2 (Enum num_enums)))), + (l,simple_annot t2))) enums), + (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) + | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))) + + (* bit vector to an enumeration type *) | Tapp("vector", [TA_nexp _; TA_nexp size; _; TA_typ {t= Tid "bit"}]), Tid(i) -> (match Envmap.apply d_env.enum_env i with | Some(enums) -> @@ -3573,19 +3684,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e (l,simple_annot t2))) enums), (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))) - | Tapp("atom",[TA_nexp b1]),Tid(i) -> - (match Envmap.apply d_env.enum_env i with - | Some(enums) -> - let num_enums = List.length enums in - (t2,[GtEq(co,Require,b1,n_zero); - LtEq(co,Require,b1,mk_c(big_int_of_int num_enums))],pure_e, - E_aux(E_case(e, - List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)),(l, simple_annot t1)), - E_aux(E_id(Id_aux(Id a,l)), - (l, tag_annot t2 (Enum num_enums)))), - (l,simple_annot t2))) enums), - (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) - | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))) + + (* enumeration type to number range *) | Tid(i),Tapp("range",[TA_nexp b1;TA_nexp r1;]) -> (match Envmap.apply d_env.enum_env i with | Some(enums) -> @@ -3596,6 +3696,11 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e (l,simple_annot t2))) enums), (l,simple_annot_efr t2 (get_cummulative_effects (get_eannot e))))) | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2))) + + + (* probably there's a missing enumeration type to singleton number range *) + + (* fall through to type_consistent *) | _,_ -> let t',cs = type_consistent co d_env enforce widen t1 t2 in (t',cs,pure_e,e) and type_coerce co d_env enforce is_explicit widen bounds t1 e t2 = diff --git a/src/type_internal.mli b/src/type_internal.mli index b55418fe..091f1e64 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -1,3 +1,45 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + open Big_int module Envmap : Finite_map.Fmap with type k = string @@ -337,3 +379,6 @@ val type_coerce : constraint_origin -> def_envs -> range_enforcement -> bool -> When merging atoms, use bool to control widening. *) val tannot_merge : constraint_origin -> def_envs -> bool -> tannot -> tannot -> tannot + +val initial_typ_env : tannot Envmap.t + diff --git a/src/util.ml b/src/util.ml index a2bd7cc0..2b6f81f8 100644 --- a/src/util.ml +++ b/src/util.ml @@ -1,4 +1,46 @@ (**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +(**************************************************************************) (* Lem *) (* *) (* Dominic Mulligan, University of Cambridge *) @@ -44,6 +86,7 @@ (* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (**************************************************************************) + module Duplicate(S : Set.S) = struct type dups = diff --git a/src/util.mli b/src/util.mli index 45e20381..c565cdce 100644 --- a/src/util.mli +++ b/src/util.mli @@ -1,47 +1,43 @@ (**************************************************************************) -(* Lem *) +(* Sail *) (* *) -(* Dominic Mulligan, University of Cambridge *) -(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) -(* Gabriel Kerneis, University of Cambridge *) -(* Kathy Gray, University of Cambridge *) -(* Peter Boehm, University of Cambridge (while working on Lem) *) -(* Peter Sewell, University of Cambridge *) -(* Scott Owens, University of Kent *) -(* Thomas Tuerk, University of Cambridge *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) (* *) -(* The Lem sources are copyright 2010-2013 *) -(* by the UK authors above and Institut National de Recherche en *) -(* Informatique et en Automatique (INRIA). *) -(* *) -(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) -(* are distributed under the license below. The former are distributed *) -(* under the LGPLv2, as in the LICENSE file. *) +(* All rights reserved. *) (* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) +(* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in the *) -(* documentation and/or other materials provided with the distribution. *) -(* 3. The names of the authors may not be used to endorse or promote *) -(* products derived from this software without specific prior written *) -(* permission. *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) (* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) -(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) -(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) -(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) -(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) -(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) -(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) -(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) -(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) -(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) -(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) (**************************************************************************) (** Mixed useful things *) |