From d7ce278ada49cbfdeeec35d12f86bcea56b4a6c9 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Sat, 16 Dec 2017 16:41:23 +0000 Subject: compatibility with OCaml 4.06.0; imported new version of PPrint (20171003) --- src/pprint/src/META | 2 +- src/pprint/src/Makefile | 15 +++++++-- src/pprint/src/PPrint.ml | 10 +++--- src/pprint/src/PPrintCombinators.ml | 10 +++--- src/pprint/src/PPrintCombinators.mli | 12 +++---- src/pprint/src/PPrintEngine.ml | 61 +++++++++++++++++++----------------- src/pprint/src/PPrintEngine.mli | 10 +++--- src/pprint/src/PPrintOCaml.ml | 10 +++--- src/pprint/src/PPrintOCaml.mli | 10 +++--- src/pprint/src/PPrintRenderer.ml | 10 +++--- src/pprint/src/PPrintTest.ml | 10 +++--- src/reporting_basic.ml | 4 +-- src/util.ml | 2 +- 13 files changed, 91 insertions(+), 75 deletions(-) diff --git a/src/pprint/src/META b/src/pprint/src/META index b7d43d40..4a966166 100755 --- a/src/pprint/src/META +++ b/src/pprint/src/META @@ -2,4 +2,4 @@ requires = "" description = "The PPrint pretty-printing library" archive(byte) = "PPrintLib.cma" archive(native) = "PPrintLib.cmxa" -version = "20140424" +version = "20171003" diff --git a/src/pprint/src/Makefile b/src/pprint/src/Makefile index f56f4d88..3bfa12df 100644 --- a/src/pprint/src/Makefile +++ b/src/pprint/src/Makefile @@ -1,6 +1,6 @@ -.PHONY: all install clean doc test +.PHONY: all install uninstall reinstall clean doc test bench -OCAMLBUILD := ocamlbuild -use-ocamlfind -cflags "-g" -lflags "-g" -classic-display +OCAMLBUILD := ocamlbuild -use-ocamlfind -classic-display OCAMLFIND := ocamlfind DOCDIR := doc MAIN := PPrintTest @@ -14,6 +14,14 @@ install: all $(patsubst %,_build/%,$(TO_BUILD)) \ _build/PPrintLib.a _build/*.cmx _build/*.cmi +# [make uninstall] attempts to uninstall, but succeeds even if uninstallation +# fails (probably because the package was not installed in the first place). +uninstall: + ocamlfind remove pprint || true + +reinstall: uninstall + @ $(MAKE) install + clean: rm -f *~ rm -rf doc @@ -33,3 +41,6 @@ test: all $(OCAMLBUILD) $(MAIN).native ./$(MAIN).native +bench: all + $(OCAMLBUILD) -tag use_unix PPrintBench.native + time ./PPrintBench.native diff --git a/src/pprint/src/PPrint.ml b/src/pprint/src/PPrint.ml index ae1ff709..46d732b1 100644 --- a/src/pprint/src/PPrint.ml +++ b/src/pprint/src/PPrint.ml @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) diff --git a/src/pprint/src/PPrintCombinators.ml b/src/pprint/src/PPrintCombinators.ml index 39b99b9c..70499878 100644 --- a/src/pprint/src/PPrintCombinators.ml +++ b/src/pprint/src/PPrintCombinators.ml @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) diff --git a/src/pprint/src/PPrintCombinators.mli b/src/pprint/src/PPrintCombinators.mli index ef2b44ea..c538cb35 100644 --- a/src/pprint/src/PPrintCombinators.mli +++ b/src/pprint/src/PPrintCombinators.mli @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) @@ -133,7 +133,7 @@ val words: string -> document list character that satisfies the predicate [ok]. The substrings thus obtained are turned into documents, and a list of documents is returned. No information is lost: the concatenation of the documents yields the - original string. This code is not UTF-8 aware. *) + original string. This code is not UTF-8 aware. *) val split: (char -> bool) -> string -> document list (** [flow sep docs] separates the documents in the list [docs] with the diff --git a/src/pprint/src/PPrintEngine.ml b/src/pprint/src/PPrintEngine.ml index cfa8474a..2a78363d 100644 --- a/src/pprint/src/PPrintEngine.ml +++ b/src/pprint/src/PPrintEngine.ml @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) @@ -57,7 +57,13 @@ end class channel_output channel = object method char = output_char channel - method substring = output channel + method substring = output_substring channel + (* We used to use [output], but, as of OCaml 4.02 and with -safe-string + enabled, the type of [output] has changed: this function now expects + an argument of type [bytes]. The new function [output_substring] must + be used instead. Furthermore, as of OCaml 4.06, -safe-string is enabled + by default. In summary, we require OCaml 4.02, use [output_substring], + and enable -safe-string. *) end class buffer_output buffer = object @@ -152,21 +158,21 @@ end type document = - (* [Empty] is the empty document. *) + (* [Empty] is the empty document. *) | Empty - (* [Char c] is a document that consists of the single character [c]. We - enforce the invariant that [c] is not a newline character. *) + (* [Char c] is a document that consists of the single character [c]. We + enforce the invariant that [c] is not a newline character. *) | Char of char - (* [String (s, ofs, len)] is a document that consists of the portion of - the string [s] delimited by the offset [ofs] and the length [len]. We - assume, but do not check, that this portion does not contain a newline - character. *) + (* [String s] is a document that consists of just the string [s]. We + assume, but do not check, that this string does not contain a newline + character. [String] is a special case of [FancyString], which takes up + less space in memory. *) - | String of string * int * int + | String of string (* [FancyString (s, ofs, len, apparent_length)] is a (portion of a) string that may contain fancy characters: color escape characters, UTF-8 or @@ -252,7 +258,8 @@ let rec requirement = function 0 | Char _ -> 1 - | String (_, _, len) + | String s -> + String.length s | FancyString (_, _, _, len) | Blank len -> len @@ -268,7 +275,7 @@ let rec requirement = function infinity | Cat (req, _, _) | Nest (req, _, _) - | Group (req, _) + | Group (req, _) | Align (req, _) -> (* These nodes store their requirement -- which is computed when the node is constructed -- so as to allow us to answer in constant time @@ -293,14 +300,8 @@ let char c = let space = char ' ' -let substring s ofs len = - if len = 0 then - empty - else - String (s, ofs, len) - let string s = - substring s 0 (String.length s) + String s let fancysubstring s ofs len apparent_length = if len = 0 then @@ -308,6 +309,9 @@ let fancysubstring s ofs len apparent_length = else FancyString (s, ofs, len, apparent_length) +let substring s ofs len = + fancysubstring s ofs len len + let fancystring s apparent_length = fancysubstring s 0 (String.length s) apparent_length @@ -467,8 +471,9 @@ let rec pretty (* assert (ok state flatten); *) continue output state cont - | String (s, ofs, len) -> - output#substring s ofs len; + | String s -> + let len = String.length s in + output#substring s 0 len; state.column <- state.column + len; (* assert (ok state flatten); *) continue output state cont @@ -566,8 +571,9 @@ let rec compact output doc cont = | Char c -> output#char c; continue output cont - | String (s, ofs, len) -> - output#substring s ofs len; + | String s -> + let len = String.length s in + output#substring s 0 len; continue output cont | FancyString (s, ofs, len, apparent_length) -> output#substring s ofs len; @@ -634,4 +640,3 @@ module ToFormatter = type channel = Format.formatter let output = new formatter_output end) - diff --git a/src/pprint/src/PPrintEngine.mli b/src/pprint/src/PPrintEngine.mli index 7f6fcf35..eda61a6c 100644 --- a/src/pprint/src/PPrintEngine.mli +++ b/src/pprint/src/PPrintEngine.mli @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) diff --git a/src/pprint/src/PPrintOCaml.ml b/src/pprint/src/PPrintOCaml.ml index 88e039ce..bee5f2a3 100644 --- a/src/pprint/src/PPrintOCaml.ml +++ b/src/pprint/src/PPrintOCaml.ml @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) diff --git a/src/pprint/src/PPrintOCaml.mli b/src/pprint/src/PPrintOCaml.mli index e1395203..119bca23 100644 --- a/src/pprint/src/PPrintOCaml.mli +++ b/src/pprint/src/PPrintOCaml.mli @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) diff --git a/src/pprint/src/PPrintRenderer.ml b/src/pprint/src/PPrintRenderer.ml index 9096eada..3449d6c3 100644 --- a/src/pprint/src/PPrintRenderer.ml +++ b/src/pprint/src/PPrintRenderer.ml @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) diff --git a/src/pprint/src/PPrintTest.ml b/src/pprint/src/PPrintTest.ml index 3e4fb2c9..37444127 100644 --- a/src/pprint/src/PPrintTest.ml +++ b/src/pprint/src/PPrintTest.ml @@ -2,12 +2,12 @@ (* *) (* PPrint *) (* *) -(* Francois Pottier, INRIA Paris-Rocquencourt *) -(* Nicolas Pouillard, IT University of Copenhagen *) +(* François Pottier, Inria Paris *) +(* Nicolas Pouillard *) (* *) -(* Copyright 2007-2014 INRIA. All rights reserved. This file is *) -(* distributed under the terms of the CeCILL-C license, as described *) -(* in the file LICENSE. *) +(* Copyright 2007-2017 Inria. All rights reserved. This file is *) +(* distributed under the terms of the GNU Library General Public *) +(* License, with an exception, as described in the file LICENSE. *) (* *) (**************************************************************************) diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml index 0a9a588f..e7812a63 100644 --- a/src/reporting_basic.ml +++ b/src/reporting_basic.ml @@ -152,9 +152,9 @@ let format_loc_source ff l = begin let (s, multi_line) = read_from_file_pos2 p1 p2 in if multi_line then - Format.fprintf ff " original input:\n%s\n" s + Format.fprintf ff " original input:\n%s\n" (Bytes.to_string s) else - Format.fprintf ff " original input: \"%s\"\n" s + Format.fprintf ff " original input: \"%s\"\n" (Bytes.to_string s) end | _ -> () diff --git a/src/util.ml b/src/util.ml index 733fff79..31a8110d 100644 --- a/src/util.ml +++ b/src/util.ml @@ -293,7 +293,7 @@ module ExtraSet = functor (S : Set.S) -> let copy_file src dst = let len = 5096 in - let b = String.make len ' ' in + let b = Bytes.make len ' ' in let read_len = ref 0 in let i = open_in_bin src in let o = open_out_bin dst in -- cgit v1.2.3 From a6b9f2bec81b43d87969eb75cbb3ef45bc1f088b Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 28 Dec 2017 13:41:16 +0000 Subject: use ocamlfind to locate lem and zarith --- src/Makefile | 35 ++++++++++++++++++++++++----------- src/_tags | 6 +++--- src/myocamlbuild.ml | 3 --- 3 files changed, 27 insertions(+), 17 deletions(-) diff --git a/src/Makefile b/src/Makefile index b33c2f42..931d9a39 100644 --- a/src/Makefile +++ b/src/Makefile @@ -48,6 +48,20 @@ # SUCH DAMAGE. # ########################################################################## +$(warning MAKECMDGOALS is $(MAKECMDGOALS)) +ifneq ($(MAKECMDGOALS),clean) +# Lem optionally vendors the zarith dependency, but currently +# we don't use that -- just assume the host system has zarith. +ifeq ($(shell ocamlfind query zarith),) +$(error No zarith installed [anywhere ocamlfind can find it]; install it (opam install zarith || apt-get install libzarith-ocaml{,-dev} || yum install ocaml-zarith), or use make install_dependencies in lem/ocaml-lib.) +endif +# assume the host system has lem +ifeq ($(shell ocamlfind query lem),) +$(error No lem installed [anywhere ocamlfind can find it]; please install it ('make install' from lem/ocaml-lib || 'make local-install' from lem/ocaml-lib and add lem/ocaml-lib/local to OCAMLPATH)) +endif +endif + + .PHONY: all sail test clean doc lib power test_power test_idempotence # set to -p on command line to enable gprof profiling @@ -58,26 +72,25 @@ all: sail lib doc full: sail lib power doc test sail: - ocamlbuild sail.native sail_lib.cma sail_lib.cmxa + ocamlbuild -use-ocamlfind sail.native sail_lib.cma sail_lib.cmxa sail.native: sail sail.byte: - ocamlbuild -cflag -g sail.byte + ocamlbuild -use-ocamlfind -cflag -g sail.byte interpreter: - ocamlbuild lem_interp/extract.cmxa - ocamlbuild lem_interp/extract.cma + ocamlbuild -use-ocamlfind lem_interp/extract.cmxa + ocamlbuild -use-ocamlfind lem_interp/extract.cma test: sail interpreter - ocamlbuild test/run_tests.native + ocamlbuild -use-ocamlfind test/run_tests.native ./run_tests.native THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) BITBUCKET_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..) LEM = $(BITBUCKET_ROOT)/lem/lem -LEMLIBOCAML = $(BITBUCKET_ROOT)/lem/ocaml-lib/_build_zarith ELFDIR= $(BITBUCKET_ROOT)/linksem SAIL_DIR:=$(BITBUCKET_ROOT)/sail @@ -200,13 +213,13 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail $(LEM) -only_changed_output -ocaml -lib lem_interp/ $< run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native run_cheri128.native: _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml interpreter - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml -o run_cheri128.native + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml -o run_cheri128.native run_embed.native: _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_embed.ml _build/cheri_embed.ml _build/cheri128_embed.ml _build/run_embed.ml env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package zarith -package unix -I _build -linkpkg $^ -o $@ @@ -241,7 +254,7 @@ clean: -rm -rf sail.docdir doc: - ocamlbuild sail.docdir/index.html + ocamlbuild -use-ocamlfind sail.docdir/index.html lib: - ocamlbuild pretty_print.cmxa pretty_print.cma + ocamlbuild -use-ocamlfind pretty_print.cmxa pretty_print.cma diff --git a/src/_tags b/src/_tags index 8ec7acb9..30e0755a 100644 --- a/src/_tags +++ b/src/_tags @@ -1,12 +1,12 @@ true: -traverse, debug <**/*.ml>: bin_annot, annot or : include -: use_pprint, use_nums +: use_pprint, package(num) or : include # see http://caml.inria.fr/mantis/view.php?id=4943 - and not : use_nums, use_lem - and not : use_nums, use_lem, use_str + and not : package(num), package(lem) + and not : package(num), package(lem), package(str) # disable partial match and unused variable warnings <**/*.ml>: warn_y diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml index 7ec72345..bd0c68c0 100644 --- a/src/myocamlbuild.ml +++ b/src/myocamlbuild.ml @@ -69,8 +69,6 @@ let split ch s = let lem_dir = try Sys.getenv "LEM_DIR" (* LEM_DIR must contain an absolute path *) with Not_found -> "../../../lem" ;; -let lem_libdir = lem_dir / "ocaml-lib" / "_build_zarith";; -let lem_lib = lem_libdir / "extract" ;; let lem = lem_dir / "lem" ;; (* All -wl ignores should be removed if you want to see the pattern compilation, exhaustive, and unused var warnings *) @@ -85,7 +83,6 @@ let lem_opts = [A "-lib"; P "../lem_interp"; dispatch begin function | After_rules -> (* ocaml_lib "lem_interp/interp"; *) - ocaml_lib ~extern:true ~dir:lem_libdir ~tag_name:"use_lem" lem_lib; ocaml_lib ~extern:false ~dir:"pprint/src" ~tag_name:"use_pprint" "pprint/src/PPrintLib"; rule "lem -> ml" -- cgit v1.2.3 From 1d22a0b403e90749eb9d97bed90c202e21b3d068 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 28 Dec 2017 14:00:02 +0000 Subject: use ocamlfind to locate lem and zarith (missed this Makefile) --- src/test/lib/Makefile | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/test/lib/Makefile b/src/test/lib/Makefile index d2185866..fbd5a332 100644 --- a/src/test/lib/Makefile +++ b/src/test/lib/Makefile @@ -8,11 +8,8 @@ TESTS=div.sail BITBUCKET_DIR:=$(realpath ../../../../) LEM_DIR:=$(BITBUCKET_DIR)/lem LEM:=$(LEM_DIR)/lem -LEMLIB = $(LEM_DIR)/ocaml-lib SAIL_DIR:=$(BITBUCKET_DIR)/sail/src SAIL:=$(SAIL_DIR)/sail.native -ZARITH_DIR:=$(LEM_DIR)/ocaml-lib/dependencies/zarith -ZARITH_LIB:=$(ZARITH_DIR)/zarith.cmxa SAIL_VALUES:=$(SAIL_DIR)/gen_lib/sail_values.ml BUILD_DIR:=_build @@ -41,14 +38,14 @@ $(BUILD_DIR)/sail_values.ml: | $(BUILD_DIR) $(BUILD_DIR)/%_embed.out : tests/%.sail $(BUILD_DIR)/run_test_embed.ml $(BUILD_DIR)/sail_values.ml cd $(BUILD_DIR) && \ $(SAIL) -ocaml ../test_prelude.sail ../$< ../test_epilogue.sail -o test && \ - ocamlopt -I $(ZARITH_DIR) $(ZARITH_LIB) sail_values.ml test.ml run_test_embed.ml -o test_embed.native && \ + ocamlfind ocamlopt -package zarith -linkpkg sail_values.ml test.ml run_test_embed.ml -o test_embed.native && \ ./test_embed.native > $(notdir $@) $(BUILD_DIR)/%_interp.out : tests/%.sail $(BUILD_DIR)/run_test_interp.ml cd $(BUILD_DIR) && \ $(SAIL) -lem_ast ../test_prelude.sail ../$< ../test_epilogue.sail -o test_lem_ast && \ $(LEM) -ocaml test_lem_ast.lem -lib $(SAIL_DIR)/lem_interp && \ - ocamlfind ocamlopt -g -package num -I $(ZARITH_DIR) -I $(SAIL_DIR)/_build/lem_interp -I $(LEMLIB) -linkpkg $(ZARITH_LIB) $(LEMLIB)/extract.cmxa $(SAIL_DIR)/_build/lem_interp/extract.cmxa test_lem_ast.ml run_test_interp.ml -o test_interp.native && \ + ocamlfind ocamlopt -g -package num -package zarith -package lem -linkpkg -I $(SAIL_DIR)/_build/lem_interp $(SAIL_DIR)/_build/lem_interp/extract.cmxa test_lem_ast.ml run_test_interp.ml -o test_interp.native && \ ./test_interp.native >$(notdir $@) 2>&1 tests.xml: $(OCAML_RESULTS) $(INTERP_RESULTS) -- cgit v1.2.3 From f1336fcf6b54a1c3e362112a540d7767355b0165 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Sat, 30 Dec 2017 10:09:13 +0000 Subject: use linksem as a package --- src/Makefile | 6 +++--- src/lem_interp/run_with_elf.ml | 12 ++++++------ src/lem_interp/run_with_elf_cheri.ml | 16 ++++++++-------- src/lem_interp/run_with_elf_cheri128.ml | 16 ++++++++-------- 4 files changed, 25 insertions(+), 25 deletions(-) diff --git a/src/Makefile b/src/Makefile index 931d9a39..44d1b8b2 100644 --- a/src/Makefile +++ b/src/Makefile @@ -213,13 +213,13 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail $(LEM) -only_changed_output -ocaml -lib lem_interp/ $< run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -package zarith -package lem -package linksem -linkpkg -I _build/lem_interp/ -I _build _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml -o run_mips.native run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -package zarith -package lem -package linksem -linkpkg -I _build/lem_interp/ -I _build _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native run_cheri128.native: _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml interpreter - env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package lem -package zarith -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml -o run_cheri128.native + env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package num -package str -package unix -package zarith -package lem -package linksem -linkpkg -I _build/lem_interp/ -I _build _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml -o run_cheri128.native run_embed.native: _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_embed.ml _build/cheri_embed.ml _build/cheri128_embed.ml _build/run_embed.ml env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt $(OCAML_OPTS) -g -package zarith -package unix -I _build -linkpkg $^ -o $@ diff --git a/src/lem_interp/run_with_elf.ml b/src/lem_interp/run_with_elf.ml index 8533827b..0dadc007 100644 --- a/src/lem_interp/run_with_elf.ml +++ b/src/lem_interp/run_with_elf.ml @@ -727,7 +727,7 @@ let initial_system_state_of_elf_file name = aarch64_register_data_all) *) | 8 (* EM_MIPS *) -> let startaddr = - let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in + let e_entry = Uint64_wrapper.of_bigint e_entry in match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with | Error.Fail s -> failwith "Failed computing entry point" | Error.Success s -> s @@ -736,11 +736,11 @@ let initial_system_state_of_elf_file name = initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in (Mips.defs, - (Mips_extras.read_memory_functions, - Mips_extras.memory_writes, - Mips_extras.memory_eas, - Mips_extras.memory_vals, - Mips_extras.barrier_functions), + (Mips_extras.mips_read_memory_functions, + Mips_extras.mips_memory_writes, + Mips_extras.mips_memory_eas, + Mips_extras.mips_memory_vals, + Mips_extras.mips_barrier_functions), [], MIPS, D_decreasing, diff --git a/src/lem_interp/run_with_elf_cheri.ml b/src/lem_interp/run_with_elf_cheri.ml index 46bc92fb..2bf84e2d 100644 --- a/src/lem_interp/run_with_elf_cheri.ml +++ b/src/lem_interp/run_with_elf_cheri.ml @@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name = match Nat_big_num.to_int e_machine with | 8 (* EM_MIPS *) -> let startaddr = - let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in + let e_entry = Uint64_wrapper.of_bigint e_entry in match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with | Error.Fail s -> failwith "Failed computing entry point" | Error.Success s -> s @@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name = initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in (Cheri.defs, - (Mips_extras.read_memory_functions, - Mips_extras.read_memory_tagged_functions, - Mips_extras.memory_writes, - Mips_extras.memory_eas, - Mips_extras.memory_vals, - Mips_extras.memory_vals_tagged, - Mips_extras.barrier_functions), + (Mips_extras.mips_read_memory_functions, + Mips_extras.mips_read_memory_tagged_functions, + Mips_extras.mips_memory_writes, + Mips_extras.mips_memory_eas, + Mips_extras.mips_memory_vals, + Mips_extras.mips_memory_vals_tagged, + Mips_extras.mips_barrier_functions), [], MIPS, D_decreasing, diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml index 5e5bee21..e4d91c41 100644 --- a/src/lem_interp/run_with_elf_cheri128.ml +++ b/src/lem_interp/run_with_elf_cheri128.ml @@ -396,7 +396,7 @@ let initial_system_state_of_elf_file name = match Nat_big_num.to_int e_machine with | 8 (* EM_MIPS *) -> let startaddr = - let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in + let e_entry = Uint64_wrapper.of_bigint e_entry in match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with | Error.Fail s -> failwith "Failed computing entry point" | Error.Success s -> s @@ -405,13 +405,13 @@ let initial_system_state_of_elf_file name = initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in (Cheri128.defs, - (Mips_extras.read_memory_functions, - Mips_extras.read_memory_tagged_functions, - Mips_extras.memory_writes, - Mips_extras.memory_eas, - Mips_extras.memory_vals, - Mips_extras.memory_vals_tagged, - Mips_extras.barrier_functions), + (Mips_extras.mips_read_memory_functions, + Mips_extras.mips_read_memory_tagged_functions, + Mips_extras.mips_memory_writes, + Mips_extras.mips_memory_eas, + Mips_extras.mips_memory_vals, + Mips_extras.mips_memory_vals_tagged, + Mips_extras.mips_barrier_functions), [], MIPS, D_decreasing, -- cgit v1.2.3 From 412a7a2e3a678362e0619aea640af9e24bc4682c Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Tue, 9 Jan 2018 12:24:21 +0000 Subject: the 'imm' of adr/adrp is signed --- arm/gen/sail_trans_out.hgen | 2 +- arm/gen/shallow_ast_to_herdtools_ast.hgen | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/arm/gen/sail_trans_out.hgen b/arm/gen/sail_trans_out.hgen index 9595f00c..84826c18 100644 --- a/arm/gen/sail_trans_out.hgen +++ b/arm/gen/sail_trans_out.hgen @@ -64,7 +64,7 @@ | "Address", [d; page; imm] -> `AArch64Address ( translate_out_regzr Set64 d, translate_out_bool page, - translate_out_big_bit imm) + translate_out_signed_big_bit imm) | "LogicalImmediate", [d; n; datasize; setflags; op; imm] -> let setflags' = translate_out_bool setflags in diff --git a/arm/gen/shallow_ast_to_herdtools_ast.hgen b/arm/gen/shallow_ast_to_herdtools_ast.hgen index aa989e95..6927767e 100644 --- a/arm/gen/shallow_ast_to_herdtools_ast.hgen +++ b/arm/gen/shallow_ast_to_herdtools_ast.hgen @@ -64,7 +64,7 @@ | Address0 (d, page, imm) -> `AArch64Address ( translate_out_regzr Set64 d, translate_out_bool page, - translate_out_big_bit imm) + translate_out_signed_big_bit imm) | LogicalImmediate (d, n, datasize, setflags, op, imm) -> let setflags' = translate_out_bool setflags in -- cgit v1.2.3 From f0963618ba927492b0724383040b9922ab41f1dd Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Wed, 10 Jan 2018 11:18:54 +0000 Subject: wib --- arm/armV8.sail | 10 +++++----- arm/armV8_A64_sys_regs.sail | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/arm/armV8.sail b/arm/armV8.sail index 2614c7a5..cfdb94f9 100644 --- a/arm/armV8.sail +++ b/arm/armV8.sail @@ -40,7 +40,7 @@ typedef ast = const union forall Nat 'R, 'R IN {32, 64}, (* register size *) ImplementationDefinedStopFetching; ImplementationDefinedThreadStart; - (* transactional memory, from the pre-alpha document *) + (* transactional memory, not part of the official spec *) (reg_index) TMStart; TMCommit; (boolean,bit[5]) TMAbort; @@ -106,7 +106,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}. Some(TMStart(t)); } -(* transactional memory, from the pre-alpha document *) +(* transactional memory, not part of the official spec *) function clause execute (TMStart(t)) = { (bit[8]) nesting := TxNestingLevel; @@ -132,7 +132,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}. Some(TMCommit); } -(* transactional memory, from the pre-alpha document *) +(* transactional memory, not part of the official spec *) function clause execute (TMCommit) = { (bit[8]) nesting := TxNestingLevel; @@ -151,7 +151,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}. Some(TMTest); } -(* transactional memory, from the pre-alpha document *) +(* transactional memory, not part of the official spec *) function clause execute (TMTest) = { if TxNestingLevel > 0 then wPSTATE_NZCV() := 0b0000 @@ -166,7 +166,7 @@ function forall Nat 'R, 'R IN {32,64}, Nat 'D, 'D IN {8,16,32,64}. Some(TMAbort(R,imm5)); } -(* transactional memory, from the pre-alpha document *) +(* transactional memory, not part of the official spec *) function clause execute (TMAbort(retry,reason)) = { if TxNestingLevel > 0 then { (bit[64]) status := 0; diff --git a/arm/armV8_A64_sys_regs.sail b/arm/armV8_A64_sys_regs.sail index 95b5c710..3a5f85fa 100644 --- a/arm/armV8_A64_sys_regs.sail +++ b/arm/armV8_A64_sys_regs.sail @@ -278,7 +278,7 @@ typedef EDSCR_type = register bits [31:0] } register (EDSCR_type) EDSCR (* External Debug Status and Control Register *) -(* transactional memory, from the pre-alpha document *) +(* transactional memory, not part of the official spec *) typedef TXIDR_EL0_type = register bits [63:0] { (*63..8 : RES0;*) -- cgit v1.2.3 From 71fa25403c7e99ca57753faf9738f37fe36ed1c1 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Thu, 18 Jan 2018 11:11:33 +0000 Subject: immediate for CIncOffsetImmediate must be treated as signed (fixes test_cp2_rep_underflow). --- cheri/cheri_insts.sail | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index 5687a275..66f87310 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -495,7 +495,7 @@ function clause execute (CIncOffsetImmediate(cd, cb, imm)) = (* START_CIncOffsetImmediate *) checkCP2usable(); cb_val := readCapReg(cb); - let (bit[64]) imm64 = EXTZ(imm) in + let (bit[64]) imm64 = EXTS(imm) in if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then -- cgit v1.2.3 From ef5eee97618d226249281bb0d2ad47c02d8f364c Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Wed, 31 Jan 2018 15:59:24 +0000 Subject: changed directory structure after migration to github --- language/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/language/Makefile b/language/Makefile index 9167d65f..b1f8502a 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=../../../github/ott/src/ott +OTT=../../ott/src/ott OTTLIB=$(dir $(shell which ott))../hol .PHONY: all -- cgit v1.2.3 From 151d86b911c9a266465638ee3514156dfb178e92 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Wed, 31 Jan 2018 16:22:12 +0000 Subject: minor rename --- src/Makefile | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Makefile b/src/Makefile index 44d1b8b2..2bd31c14 100644 --- a/src/Makefile +++ b/src/Makefile @@ -88,12 +88,12 @@ test: sail interpreter ./run_tests.native THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) -BITBUCKET_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..) +PROJECT_ROOT=$(realpath $(dir $(THIS_MAKEFILE))../..) -LEM = $(BITBUCKET_ROOT)/lem/lem -ELFDIR= $(BITBUCKET_ROOT)/linksem +LEM = $(PROJECT_ROOT)/lem/lem +ELFDIR= $(PROJECT_ROOT)/linksem -SAIL_DIR:=$(BITBUCKET_ROOT)/sail +SAIL_DIR:=$(PROJECT_ROOT)/sail MIPS_SAIL_DIR:=$(SAIL_DIR)/mips MIPS_SAILS_PRE:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail -- cgit v1.2.3 From 043ea8ec3faecadf34ef9010bdd539f595f9c6da Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 8 Feb 2018 12:06:00 +0000 Subject: replaced NIA_LR/CTR/register with NIA_indirect; removed IK_cond_branch, and added IK_branch --- Makefile | 25 ++++++++++++++++--- arm/Makefile | 2 +- arm/aarch64_regfp.sail | 12 ++++----- arm/armV8.sail | 2 +- etc/regfp.sail | 6 ++--- mips/mips_regfp.sail | 16 +++++------- power/power_regfp.sail | 16 ++++++------ risc-v/riscv_regfp.sail | 10 +++++--- src/gen_lib/deep_shallow_convert.lem | 4 +-- src/gen_lib/sail_values.lem | 8 ++---- src/lem_interp/interp_inter_imp.lem | 48 +++++++++++++----------------------- src/lem_interp/sail_impl_base.lem | 41 +++++++++--------------------- x86/x64.sail | 13 ++++------ 13 files changed, 90 insertions(+), 113 deletions(-) diff --git a/Makefile b/Makefile index 97e42f7e..2b5e867c 100644 --- a/Makefile +++ b/Makefile @@ -1,24 +1,35 @@ -.PHONY: all sail language clean archs isabelle-lib apply_header +ARCHS += power +ARCHS += arm +ARCHS += risc-v +# ARCHS += mips +# ARCHS += cheri +ARCHS += x86 all: sail interpreter +.PHONY: all sail: $(MAKE) -C src ln -f -s src/sail.native sail +.PHONY: sail language: $(MAKE) -C language +.PHONY: language -interpreter: +interpreter: $(MAKE) -C src interpreter +.PHONY: interpreter archs: - for arch in arm mips cheri; do\ + for arch in $(ARCHS); do\ $(MAKE) -C "$$arch" || exit;\ done +.PHONY: archs isabelle-lib: $(MAKE) -C isabelle-lib +.PHONY: isabelle-lib apply_header: $(MAKE) clean @@ -29,9 +40,17 @@ apply_header: 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 +.PHONY: apply_header clean: for subdir in src arm ; do\ $(MAKE) -C "$$subdir" clean;\ done -rm sail +.PHONY: clean + +clean_archs: + for arch in $(ARCHS); do\ + $(MAKE) -C "$$arch" clean;\ + done +.PHONY: clean_archs diff --git a/arm/Makefile b/arm/Makefile index d7124df6..c597f714 100644 --- a/arm/Makefile +++ b/arm/Makefile @@ -38,7 +38,7 @@ apply_header: .PHONY: apply_header ###################################################################### -IDLARM=../../../rsem/idlarm +IDLARM=../../rsem/idlarm pull_from_idlarm: $(MAKE) -C $(IDLARM) clean diff --git a/arm/aarch64_regfp.sail b/arm/aarch64_regfp.sail index 148f9646..60aa48d1 100644 --- a/arm/aarch64_regfp.sail +++ b/arm/aarch64_regfp.sail @@ -168,7 +168,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; (bit[64]) nia' := rPC() + offset; Nias := [|| NIAFP_successor, NIAFP_concrete_address(nia') ||]; - ik := IK_cond_branch; + ik := IK_branch; } case (BranchConditional(offset,condition)) -> { iR := append(iR,ConditionHoldsIFP(condition)); @@ -176,7 +176,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia ConditionHolds(condition) *) let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; Nias := [|| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) ||]; - ik := IK_cond_branch; + ik := IK_branch; } case (GenerateExceptionEL1(imm)) -> not_implemented("GenerateExceptionEL1") case (GenerateExceptionEL2(imm)) -> not_implemented("GenerateExceptionEL2") @@ -271,14 +271,14 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia operand[bit_pos] == bit_val *) let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; Nias := [|| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) ||]; - ik := IK_cond_branch; + ik := IK_branch; } case (BranchImmediate(branch_type,offset)) -> { if branch_type == BranchType_CALL then {iR := _PCfp :: iR; oR := append(xFP(30),oR)}; let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; Nias := [|| NIAFP_concrete_address(rPC() + offset) ||]; - ik := IK_simple (* IK_uncond_branch *) + ik := IK_branch } case (BranchRegister(n,branch_type)) -> { iR := append(iR,xFP(n)); @@ -287,8 +287,8 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) effect pure initia let (i,o) = BranchToFP(iR,oR) in {iR := i; oR := o}; Nias := if n ==31 then [|| NIAFP_concrete_address(0) ||] - else [|| NIAFP_register(RFull(_Rs[n]))||]; - ik := IK_simple (* IK_uncond_branch *) + else [|| NIAFP_indirect_address ||]; + ik := IK_branch } case (ExceptionReturn) -> not_implemented("ExceptionReturn") case (DebugRestorePState) -> not_implemented("DebugRestorePState") diff --git a/arm/armV8.sail b/arm/armV8.sail index cfdb94f9..4a62bda6 100644 --- a/arm/armV8.sail +++ b/arm/armV8.sail @@ -642,7 +642,7 @@ function clause execute (BranchRegister(n,branch_type)) = (bit[64]) target := rX(n); if branch_type == BranchType_CALL then wX(30) := rPC() + 4; - BranchTo(target, branch_type); + BranchTo(target, branch_type); } (* ERET *) diff --git a/etc/regfp.sail b/etc/regfp.sail index cc057f2e..9a6172a9 100644 --- a/etc/regfp.sail +++ b/etc/regfp.sail @@ -16,9 +16,7 @@ typedef regfps = list typedef niafp = const union { NIAFP_successor; (bit[64]) NIAFP_concrete_address; - NIAFP_LR; - NIAFP_CTR; - (regfp) NIAFP_register; + NIAFP_indirect_address; } typedef niafps = list @@ -90,7 +88,7 @@ typedef instruction_kind = const union { (read_kind) IK_mem_read; (write_kind) IK_mem_write; (read_kind, write_kind) IK_mem_rmw; - IK_cond_branch; + IK_branch; (trans_kind) IK_trans; IK_simple } diff --git a/mips/mips_regfp.sail b/mips/mips_regfp.sail index 36750583..13165f67 100644 --- a/mips/mips_regfp.sail +++ b/mips/mips_regfp.sail @@ -322,38 +322,34 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( oR := RFull("HI") :: RFull ("LO") :: oR; } case (J(offset)) -> { - (* XXX actually unconditional jump *) - (*ik := IK_cond_branch;*) + ik := IK_branch; Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00); } case (JAL(offset)) -> { - (* XXX actually unconditional jump *) - (*ik := IK_cond_branch;*) + ik := IK_branch; oR := RFull("GPR31") :: oR; Dia := DIAFP_concrete((PC + 4)[63..28] : offset : 0b00); } case (JR(rs)) -> { - (* XXX actually unconditional jump *) - (*ik := IK_cond_branch;*) + ik := IK_branch; iR := RFull(GPRs[rs]) :: iR; Dia := DIAFP_reg(RFull(GPRs[rs])); } case (JALR(rs, rd)) -> { - (* XXX actually unconditional jump *) - (*ik := IK_cond_branch;*) + ik := IK_branch; iR := RFull(GPRs[rs]) :: iR; oR := RFull("GPR31") :: oR; Dia := DIAFP_reg(RFull(GPRs[rs])); } case (BEQ(rs, rd, imm, ne, likely)) -> { - ik := IK_cond_branch; + ik := IK_branch; if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; if rd == 0 then () else iR := RFull(GPRs[rd]) :: iR; let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in Dia := DIAFP_concrete (PC + offset); } case (BCMPZ(rs, imm, cmp, link, likely)) -> { - ik := IK_cond_branch; + ik := IK_branch; if rs == 0 then () else iR := RFull(GPRs[rs]) :: iR; if link then oR := RFull("GPR31") :: oR; diff --git a/power/power_regfp.sail b/power/power_regfp.sail index 35ecb37b..1f421186 100644 --- a/power/power_regfp.sail +++ b/power/power_regfp.sail @@ -76,7 +76,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( if LK then oR := RFull("LR") :: oR; (bit[64]) nia' := if AA then EXTS(LI : 0b00) else CIA + EXTS(LI : 0b00); Nias := [|| NIAFP_concrete_address(nia') ||]; - ik := IK_simple (* IK_uncond_branch *); + ik := IK_branch } case (Bc (BO, BI, BD, AA, LK)) -> { iR := mode64bit_fp :: iR; @@ -89,7 +89,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( if AA then iR := CIA_fp :: iR; Nias := [|| NIAFP_successor, NIAFP_concrete_address(if AA then EXTS(BD : 0b00) else CIA + EXTS(BD : 0b00)) ||]; if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR}; - ik := IK_cond_branch + ik := IK_branch } case (Bclr (BO, BI, BH, LK)) -> { iR := mode64bit_fp :: iR; @@ -99,18 +99,18 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( (* TODO: actually whether LR is read, NIA written depends on runtime data *) (* if ctr_ok .. *) iR := RSlice("LR",0,61) :: iR; oR := NIA_fp :: oR; - Nias := [|| NIAFP_successor, NIAFP_LR ||]; + Nias := [|| NIAFP_successor, NIAFP_indirect_address ||]; if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR;}; - ik := IK_cond_branch; + ik := IK_branch; } case (Bcctr (BO, BI, BH, LK)) -> { iR := RSliceBit("CR",BI + 32) :: iR; (* TODO: actually whether CTR is read and NIA written depends on runtime data *) (* if cond_ok *) iR := RSlice("CTR",0,61) :: iR; oR := NIA_fp :: oR; - Nias := [|| NIAFP_successor, NIAFP_CTR ||]; + Nias := [|| NIAFP_successor, NIAFP_indirect_address ||]; if LK then {oR := RFull("LR") :: oR; iR := CIA_fp :: iR;}; - ik := IK_cond_branch; + ik := IK_branch; } case (Crand (BT, BA, BB)) -> { iR := RSliceBit("CR",BA + 32) :: RSliceBit("CR",BB + 32) :: iR; @@ -150,7 +150,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( } case (Sc (LEV)) -> { (* fake test end instruction *) - Nias := if LEV==63 then [|| ||] else [|| NIAFP_successor ||]; + (); } case (Scv (LEV)) -> () case (Lbz (RT, RA, D)) -> { @@ -1480,4 +1480,4 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) recalculate_stswx_ }; ik := IK_mem_write(Write_plain); (iR,oR,aR,Nias,Dia,ik)} -} \ No newline at end of file +} diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail index dee9cc8e..5bbcf044 100644 --- a/risc-v/riscv_regfp.sail +++ b/risc-v/riscv_regfp.sail @@ -23,20 +23,22 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( case (RISCV_JAL ( imm, rd)) -> { if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; let (bit[64]) offset = EXTS(imm) in - Nias := [|| NIAFP_concrete_address (PC + offset) ||] + Nias := [|| NIAFP_concrete_address (PC + offset) ||]; + ik := IK_branch; } case (RISCV_JALR ( imm, rs, rd)) -> { if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; if (rd == 0) then () else oR := RFull(GPRstr[rd]) :: oR; let (bit[64]) offset = EXTS(imm) in - Nias := [|| NIAFP_register (RFull(GPRstr[rs])) ||]; + Nias := [|| NIAFP_indirect_address ||]; + ik := IK_branch; } case (BTYPE ( imm, rs2, rs1, op)) -> { if (rs2 == 0) then () else iR := RFull(GPRstr[rs2]) :: iR; if (rs1 == 0) then () else iR := RFull(GPRstr[rs1]) :: iR; - ik := IK_cond_branch; + ik := IK_branch; let (bit[64]) offset = EXTS(imm) in - Nias := NIAFP_concrete_address(PC + offset) :: Nias; + Nias := [|| NIAFP_concrete_address(PC + offset), NIAFP_successor ||]; } case (ITYPE ( imm, rs, rd, op)) -> { if (rs == 0) then () else iR := RFull(GPRstr[rs]) :: iR; diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem index 76880dbd..7fea0409 100644 --- a/src/gen_lib/deep_shallow_convert.lem +++ b/src/gen_lib/deep_shallow_convert.lem @@ -532,7 +532,7 @@ let instruction_kindToInterpValue = function | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_mem_rmw v -> V_ctor (Id_aux (Id "IK_mem_rmw") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) - | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) + | IK_branch -> V_ctor (Id_aux (Id "IK_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) | IK_trans v -> V_ctor (Id_aux (Id "IK_trans") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v) | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ()) end @@ -541,7 +541,7 @@ let rec instruction_kindFromInterpValue v = match v with | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v) | V_ctor (Id_aux (Id "IK_mem_rmw") _) _ _ v -> IK_mem_rmw (fromInterpValue v) - | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch + | V_ctor (Id_aux (Id "IK_branch") _) _ _ v -> IK_branch | V_ctor (Id_aux (Id "IK_trans") _) _ _ v -> IK_trans (fromInterpValue v) | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple | V_tuple [v] -> instruction_kindFromInterpValue v diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 121f6cc8..ffccaa7e 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -912,9 +912,7 @@ type regfp = type niafp = | NIAFP_successor | NIAFP_concrete_address of vector bitU - | NIAFP_LR - | NIAFP_CTR - | NIAFP_register of regfp + | NIAFP_indirect_address (* only for MIPS *) type diafp = @@ -946,9 +944,7 @@ end let niafp_to_nia reginfo = function | NIAFP_successor -> NIA_successor | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v) - | NIAFP_LR -> NIA_LR - | NIAFP_CTR -> NIA_CTR - | NIAFP_register r -> NIA_register (regfp_to_reg reginfo r) + | NIAFP_indirect_address -> NIA_indirect_address end let diafp_to_dia reginfo = function diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 2b754e25..9603b9fe 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -571,13 +571,11 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) | _ -> failwith "Register footprint analysis did not return dia of expected type" end in let nia_to_nia = function - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _ -> NIA_successor | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address -> NIA_concrete_address (get_addr address) - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR - | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg -> - NIA_register (reg_to_reg_name reg) + | Interp_ast.V_ctor (Id_aux (Id "NIAFP_indirect_address") _) _ _ _ -> + NIA_indirect_address | _ -> failwith "Register footprint analysis did not return nia of expected type" end in let readk_to_readk = function | "Read_plain" -> Read_plain @@ -634,8 +632,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis (Interp_ast.V_tuple [(Interp_ast.V_ctor (Id_aux (Id readk) _) _ _ _) ; (Interp_ast.V_ctor (Id_aux (Id writek) _) _ _ _)]) -> IK_mem_rmw(readk_to_readk readk, writek_to_writek writek) - | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ -> - IK_cond_branch + | Interp_ast.V_ctor (Id_aux (Id "IK_branch") _) _ _ _ -> + IK_branch | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ -> IK_simple | _ -> failwith "Analysis returned unexpected instruction kind" @@ -1157,7 +1155,7 @@ let rr_interp_exhaustive mode i_state events = *) -let instruction_kind_of_event : event -> maybe instruction_kind = function +let instruction_kind_of_event nia_reg : event -> maybe instruction_kind = function (* this is a hack to avoid adding special events for AArch64 transactional-memory *) | E_read_reg (Reg "TMStartEffect" 63 64 D_decreasing) -> Just (IK_trans Transaction_start) | E_write_reg (Reg "TMAbortEffect" 63 64 D_decreasing) _ -> Just (IK_trans Transaction_abort) @@ -1173,7 +1171,9 @@ let instruction_kind_of_event : event -> maybe instruction_kind = function | E_barrier bk -> Just (IK_barrier bk) | E_footprint -> Nothing | E_read_reg _ -> Nothing - | E_write_reg _ _ -> Nothing + | E_write_reg reg _ -> + if register_base_name reg = register_base_name nia_reg then Just IK_branch + else Nothing | E_error s -> failwith ("instruction_kind_of_event error: "^s) | E_escape -> Nothing (*failwith ("instruction_kind_of_event escape")*) end @@ -1252,8 +1252,8 @@ let interp_instruction_analysis (interp_exhaustive : ((list (reg_name * register_value)) -> list event)) instruction nia_reg - (nias_function : (list (maybe address) -> list reg_name -> list nia)) - ism environment = + (nias_function : (list (maybe address) -> list nia)) + ism environment = let es = interp_exhaustive environment in @@ -1263,19 +1263,15 @@ let interp_instruction_analysis let regs_feeding_address = List.concatMap regs_feeding_memory_access_address_of_event es in let nia_address = List.mapMaybe (nia_address_of_event nia_reg) es in - - let nias = nias_function nia_address regs_in in + let nias = nias_function nia_address in let dia = DIA_none in (* FIX THIS! *) - let inst_kind = - match List.mapMaybe instruction_kind_of_event es with - | [] -> if List.length nias > 1 then IK_cond_branch else IK_simple + match List.mapMaybe (instruction_kind_of_event nia_reg) es with + | [] -> IK_simple + | inst_kind :: [] -> inst_kind | inst_kind :: inst_kinds -> - let () = ensure (List.length nias > 1 --> inst_kind = IK_cond_branch) - "multiple NIAs must be IK_cond_branch" in - if forall (inst_kind' MEM inst_kinds). inst_kind' = inst_kind then inst_kind @@ -1286,19 +1282,9 @@ let interp_instruction_analysis | IK_mem_write _ -> true | IK_mem_rmw _ -> false | IK_barrier _ -> false - | IK_cond_branch -> false + | IK_branch -> false | IK_trans _ -> false | IK_simple -> false - end) && - (exists (inst_kind' MEM (inst_kind :: inst_kinds)). - match inst_kind' with - | IK_mem_read _ -> true - | _ -> false - end) && - (exists (inst_kind' MEM (inst_kind :: inst_kinds)). - match inst_kind' with - | IK_mem_write _ -> true - | _ -> false end) then match @@ -1355,7 +1341,7 @@ let interp_compare_analyses interp_exhaustive (instruction : Interp_ast.value) nia_reg - (nias_function : (list (maybe address) -> list reg_name -> list nia)) + (nias_function : (list (maybe address) -> list nia)) ism environment analysis_function diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index de3ba319..c7e01815 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -559,10 +559,9 @@ type instruction_kind = | IK_mem_read of read_kind | IK_mem_write of write_kind | IK_mem_rmw of (read_kind * write_kind) - | IK_cond_branch - (* unconditional branches are not distinguished in the instruction_kind; - they just have particular nias (and will be IK_simple *) - (* | IK_uncond_branch *) + | IK_branch (* this includes conditional-branch (multiple nias, none of which is NIA_indirect_address), + indirect/computed-branch (single nia of kind NIA_indirect_address) + and branch/jump (single nia of kind NIA_concrete_address) *) | IK_trans of trans_kind | IK_simple @@ -573,7 +572,7 @@ instance (Show instruction_kind) | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) | IK_mem_rmw (r, w) -> "IK_mem_rmw " ^ (show r) ^ " " ^ (show w) - | IK_cond_branch -> "IK_cond_branch" + | IK_branch -> "IK_branch" | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) | IK_simple -> "IK_simple" end @@ -1232,32 +1231,18 @@ end type nia = | NIA_successor | NIA_concrete_address of address - | NIA_LR (* "LR0:61 || 0b00" in Power pseudocode *) - | NIA_CTR (* "CTR0:61 || 0b00" in Power pseudocode *) - | NIA_register of reg_name (* the address will be in a register, - corresponds to AArch64 BLR, BR, RET - instructions *) + | NIA_indirect_address let niaCompare n1 n2 = match (n1,n2) with | (NIA_successor, NIA_successor) -> EQ | (NIA_successor, _) -> LT - | (NIA_concrete_address _, NIA_successor) -> GT + | (_, NIA_successor) -> GT | (NIA_concrete_address a1, NIA_concrete_address a2) -> compare a1 a2 | (NIA_concrete_address _, _) -> LT - | (NIA_LR, NIA_successor) -> GT - | (NIA_LR, NIA_concrete_address _) -> GT - | (NIA_LR, NIA_LR) -> EQ - | (NIA_LR, _) -> LT - | (NIA_CTR, NIA_successor) -> GT - | (NIA_CTR, NIA_concrete_address _) -> GT - | (NIA_CTR, NIA_LR) -> GT - | (NIA_CTR, NIA_CTR) -> EQ - | (NIA_CTR, NIA_register _) -> LT - | (NIA_register _, NIA_successor) -> GT - | (NIA_register _, NIA_concrete_address _) -> GT - | (NIA_register _, NIA_LR) -> GT - | (NIA_register _, NIA_CTR) -> GT - | (NIA_register r1, NIA_register r2) -> compare r1 r2 + | (_, NIA_concrete_address _) -> GT + | (NIA_indirect_address, NIA_indirect_address) -> EQ + (* | (NIA_indirect_address, _) -> LT + | (_, NIA_indirect_address) -> GT *) end instance (Ord nia) @@ -1269,11 +1254,9 @@ instance (Ord nia) end let stringFromNia = function - | NIA_successor -> "NIA_successor" + | NIA_successor -> "NIA_successor" | NIA_concrete_address a -> "NIA_concrete_address " ^ show a - | NIA_LR -> "NIA_LR" - | NIA_CTR -> "NIA_CTR" - | NIA_register r -> "NIA_register " ^ show r + | NIA_indirect_address -> "NIA_indirect_address" end instance (Show nia) diff --git a/x86/x64.sail b/x86/x64.sail index 9fa0b838..3549b123 100644 --- a/x86/x64.sail +++ b/x86/x64.sail @@ -1457,8 +1457,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( oR := RFull("RSP") :: oR; aR := ars; Nias := switch irm { - (* XXX register name is not important here -- just indicates we don't know the destination yet. *) - case (Rm (v)) -> NIAFP_register(RFull("RAX")) + case (Rm (v)) -> NIAFP_indirect_address case (Imm (v)) -> NIAFP_concrete_address(RIP + v) } :: Nias; } @@ -1486,7 +1485,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( case(HLT ) -> () case(Jcc (c, imm64) ) -> let flags = regfp_cond(c) in { - ik := IK_cond_branch; + ik := IK_branch; iR := RFull("RIP") :: flags; Nias := NIAFP_concrete_address(RIP + imm64) :: Nias; } @@ -1495,8 +1494,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( ik := if m then IK_mem_read(Read_plain) else IK_simple; iR := RFull("RIP")::append(rs, ars); aR := ars; - (* XXX register name is not important here -- just indicates we don't know the destination yet. *) - Nias := NIAFP_register(RFull("RAX")) :: Nias; + Nias := NIAFP_indirect_address :: Nias; } case(LEA (sz, ds) ) -> let (_, irs, ors, ars) = regfp_dest_src (ds) in { @@ -1512,7 +1510,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( } case(LOOP (c, imm64) ) -> let flags = regfp_cond(c) in { - ik := IK_cond_branch; + ik := IK_branch; iR := RFull("RCX") :: flags; oR := RFull("RCX") :: oR; Nias := NIAFP_concrete_address(RIP + imm64) :: Nias; @@ -1578,8 +1576,7 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( iR := RFull("RSP") :: iR; oR := RFull("RSP") :: oR; aR := RFull("RSP") :: aR; - (* XXX register name is not important here -- just indicates we don't know the destination yet. *) - Nias := NIAFP_register(RFull("RAX")) :: Nias; + Nias := NIAFP_indirect_address :: Nias; } case(SET (c, b, r_m) ) -> let flags = regfp_cond(c) in -- cgit v1.2.3 From 89f5441538355e98d236f85582daa12af1064722 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Tue, 13 Feb 2018 09:30:21 +0000 Subject: added footprint for sc.w/d.aq.rl (the strong, SC like, store-conditional) --- risc-v/riscv_regfp.sail | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/risc-v/riscv_regfp.sail b/risc-v/riscv_regfp.sail index 5bbcf044..55607eb4 100644 --- a/risc-v/riscv_regfp.sail +++ b/risc-v/riscv_regfp.sail @@ -124,7 +124,8 @@ function (regfps,regfps,regfps,niafps,diafp,instruction_kind) initial_analysis ( ik := switch (aq, rl) { case (false, false) -> IK_mem_write (Write_RISCV_conditional) case (false, true) -> IK_mem_write (Write_RISCV_conditional_release) - case (true, _) -> exit "not implemented" + case (true, false) -> exit "not implemented" + case (true, true) -> IK_mem_write (Write_RISCV_conditional_strong_release) }; } case (AMO( op, aq, rl, rs2, rs1, width, rd)) -> { -- cgit v1.2.3