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(-) (limited to 'src') 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(-) (limited to 'src') 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(-) (limited to 'src') 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(-) (limited to 'src') 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 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(-) (limited to 'src') 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 --- 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 +++++++++--------------------- 4 files changed, 33 insertions(+), 68 deletions(-) (limited to 'src') 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) -- cgit v1.2.3