switch to safe_string, use functions from Util

palmskog · palmskog · commit 8cfd6a2cf09c · 2017-05-26T21:26:12.000-05:00
diff --git a/README.md b/README.md
@@ -10,24 +10,33 @@ Requirements
 
 Definitions and proofs:
 
-- [`Coq 8.5`](https://coq.inria.fr/coq-85)
+- [`Coq 8.6`](https://coq.inria.fr/coq-86)
 - [`Verdi`](https://github.com/uwplse/verdi)
 - [`math-comp`](https://math-comp.github.io/math-comp/) (`ssreflect`, `fingroup`, `algebra`)
 - [`StructTact`](https://github.com/uwplse/StructTact)
 - [`InfSeqExt`](https://github.com/DistributedComponents/InfSeqExt)
 - [`AAC_tactics`](https://github.com/coq-contribs/aac-tactics)
+- [`Cheerios`](https://github.com/uwplse/cheerios)
 - [`verdi-cheerios`](https://github.com/DistributedComponents/verdi-cheerios)
 
 Executable code:
 
-- [`OCaml 4.02.3`](https://ocaml.org)
+- [`OCaml 4.02.3`](https://ocaml.org) (or later)
 - [`OCamlbuild`](https://github.com/ocaml/ocamlbuild)
 - [`ocamlfind`](http://projects.camlcity.org/projects/findlib.html)
 - [`verdi-runtime`](https://github.com/DistributedComponents/verdi-runtime)
 - [`Uuidm`](http://erratique.ch/software/uuidm)
 - [`PortAudio`](http://www.portaudio.com)
 - [`ocaml-portaudio`](https://github.com/savonet/ocaml-portaudio)
 
+Integration testing of executable code:
+
+- [`Python 2.7`](https://www.python.org/download/releases/2.7/)
+
+Unit testing of unverified code:
+
+- [`OUnit 2.0.0`](http://ounit.forge.ocamlcore.org)
+
 Building
 --------
 
@@ -38,12 +47,12 @@ The recommended way to install the OCaml and Coq dependencies of Verdi Aggregati
 ```
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
-opam install coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-aac-tactics
-opam install verdi StructTact InfSeqExt verdi-cheerios verdi-runtime uuidm portaudio
+opam install coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-aac-tactics \
+ verdi StructTact InfSeqExt cheerios verdi-cheerios verdi-runtime uuidm portaudio
 ```
 
 Then, run `./configure` in the root directory.  This will check for the appropriate version of Coq and ensure all necessary dependencies can be located.
 
-By default, the script assumes that `Verdi`, `StructTact`, `InfSeqExt`, and `VerdiCheerios` are installed in Coq's `user-contrib` directory, but this can be overridden by setting the `Verdi_PATH`, `StructTact_PATH`, `InfSeqExt_PATH`, and `VerdiCheerios_PATH` environment variables.
+By default, the script assumes that `Verdi`, `StructTact`, `InfSeqExt`, `Cheerios`, and `VerdiCheerios` are installed in Coq's `user-contrib` directory, but this can be overridden by setting the `Verdi_PATH`, `StructTact_PATH`, `InfSeqExt_PATH`, `Cheerios_PATH`, and `VerdiCheerios_PATH` environment variables.
 
 Finally, run `make` in the root directory.
diff --git a/extraction/aggregation-dynamic/Makefile b/extraction/aggregation-dynamic/Makefile
@@ -1,15 +1,14 @@
 PYTHON=python2.7
 
-OCAMLBUILD = ocamlbuild -use-ocamlfind -tag thread -package 'uuidm verdi-runtime portaudio bigarray' -I ocaml -cflag -g
-OCAMLBUILD_TEST = $(OCAMLBUILD) -package oUnit -I test
+OCAMLBUILD = ocamlbuild -use-ocamlfind -tags 'thread safe_string' -pkgs 'uuidm verdi-runtime portaudio bigarray' -I ocaml -cflag -g
+OCAMLBUILD_TEST = $(OCAMLBUILD) -pkg oUnit -I test
 
 MLEXTRACTED = ocaml/TreeAggregation.ml ocaml/TreeAggregation.mli
 
 MLFILES = ocaml/TreeAggregationArrangement.ml ocaml/TreeAggregationMain.ml \
  ocaml/Serialization.ml ocaml/Record.ml ocaml/SerializationIntPair.ml ocaml/TreeAggregationOpts.ml
 
-MLFILES_TEST = test/SerializationTest.ml test/OptsTest.ml \
-  test/TreeAggregationTest.ml test/TestCommon.ml
+MLFILES_TEST = test/SerializationTest.ml test/OptsTest.ml test/TreeAggregationTest.ml test/UtilTest.ml
 
 default: TreeAggregationMain.native
 
diff --git a/extraction/aggregation-dynamic/test/OptsTest.ml b/extraction/aggregation-dynamic/test/OptsTest.ml
@@ -1,6 +1,6 @@
 open OUnit2
 open ListLabels
-open TestCommon
+open Util
 
 let tear_down () test_ctxt =
   Opts.cluster := Opts.cluster_default;
diff --git a/extraction/aggregation-dynamic/test/TestCommon.ml b/extraction/aggregation-dynamic/test/TestCommon.ml
diff --git a/extraction/aggregation/Makefile b/extraction/aggregation/Makefile
@@ -1,15 +1,11 @@
 PYTHON=python2.7
 
-OCAMLBUILD = ocamlbuild -package uuidm -package verdi-runtime -I ocaml -cflag -g
-OCAMLBUILD_TEST = $(OCAMLBUILD) -package oUnit -I test
+OCAMLBUILD = ocamlbuild -tag safe_string -pkgs 'uuidm verdi-runtime' -I ocaml -cflag -g
+OCAMLBUILD_TEST = $(OCAMLBUILD) -pkg oUnit -I test
 
 MLEXTRACTED = ocaml/TreeAggregation.ml ocaml/TreeAggregation.mli
-
-MLFILES = ocaml/TreeAggregationArrangement.ml ocaml/TreeAggregationMain.ml \
- ocaml/Serialization.ml
-
-MLFILES_TEST = test/SerializationTest.ml test/OptsTest.ml \
- test/TreeAggregationTest.ml test/TestCommon.ml
+MLFILES = ocaml/TreeAggregationArrangement.ml ocaml/TreeAggregationMain.ml ocaml/Serialization.ml
+MLFILES_TEST = test/SerializationTest.ml test/OptsTest.ml test/TreeAggregationTest.ml test/UtilTest.ml
 
 default: TreeAggregationMain.native
 
diff --git a/extraction/aggregation/test/OptsTest.ml b/extraction/aggregation/test/OptsTest.ml
@@ -1,6 +1,6 @@
 open OUnit2
 open ListLabels
-open TestCommon
+open Util
 
 let tear_down () text_ctxt =
   Opts.cluster := Opts.cluster_default;
diff --git a/extraction/aggregation/test/TestCommon.ml b/extraction/aggregation/test/TestCommon.ml
diff --git a/extraction/tree-dynamic/Makefile b/extraction/tree-dynamic/Makefile
@@ -1,10 +1,8 @@
-OCAMLBUILD = ocamlbuild -package uuidm -package verdi-runtime -I ocaml -cflag -g
-OCAMLBUILD_TEST = $(OCAMLBUILD) -package oUnit -I test
+OCAMLBUILD = ocamlbuild -tag safe_string -pkgs 'uuidm verdi-runtime' -I ocaml -cflag -g
+OCAMLBUILD_TEST = $(OCAMLBUILD) -pkg oUnit -I test
 
 MLEXTRACTED = ocaml/Tree.ml ocaml/Tree.mli
-
 MLFILES = ocaml/TreeArrangement.ml ocaml/TreeMain.ml ocaml/Serialization.ml
-
 MLFILES_TEST = test/SerializationTest.ml test/TreeTest.ml
 
 default: TreeMain.native
diff --git a/extraction/tree/Makefile b/extraction/tree/Makefile
@@ -1,10 +1,8 @@
-OCAMLBUILD = ocamlbuild -package uuidm -package verdi-runtime -I ocaml -cflag -g
-OCAMLBUILD_TEST = $(OCAMLBUILD) -package oUnit -I test
+OCAMLBUILD = ocamlbuild -tag safe_string -pkgs 'uuidm verdi-runtime' -I ocaml -cflag -g
+OCAMLBUILD_TEST = $(OCAMLBUILD) -pkg oUnit -I test
 
 MLEXTRACTED = ocaml/Tree.ml ocaml/Tree.mli
-
 MLFILES = ocaml/TreeArrangement.ml ocaml/TreeMain.ml ocaml/Serialization.ml
-
 MLFILES_TEST = test/SerializationTest.ml test/TreeTest.ml
 
 default: TreeMain.native
diff --git a/extraction/zaggregation-dynamic/Makefile b/extraction/zaggregation-dynamic/Makefile
@@ -1,13 +1,11 @@
 PYTHON=python2.7
 
-OCAMLBUILD = ocamlbuild -use-ocamlfind -tag thread -package 'uuidm verdi-runtime' -I ocaml -cflag -g
-OCAMLBUILD_TEST = $(OCAMLBUILD) -package oUnit -I test
+OCAMLBUILD = ocamlbuild -use-ocamlfind -tags 'thread safe_string' -pkgs 'uuidm verdi-runtime' -I ocaml -cflag -g
+OCAMLBUILD_TEST = $(OCAMLBUILD) -pkg oUnit -I test
 
 MLEXTRACTED = ocaml/ZTreeAggregation.ml ocaml/ZTreeAggregation.mli
-
 MLFILES = ocaml/ZTreeAggregationArrangement.ml ocaml/ZTreeAggregationMain.ml ocaml/Serialization.ml
-
-MLFILES_TEST = test/SerializationTest.ml test/ZTreeAggregationTest.ml test/TestCommon.ml
+MLFILES_TEST = test/SerializationTest.ml test/ZTreeAggregationTest.ml test/OptsTest.ml
 
 default: ZTreeAggregationMain.native
 
diff --git a/extraction/zaggregation-dynamic/ocaml/ZTreeAggregationArrangement.ml b/extraction/zaggregation-dynamic/ocaml/ZTreeAggregationArrangement.ml
@@ -16,7 +16,7 @@ module ZTreeAggregationArrangement (P : Params) = struct
   type client_id = string
   type res = (output list * state) * ((name * msg) list)
   type task_handler = name -> state -> res
-  type timeout_setter = name -> state -> float
+  type timeout_setter = name -> state -> float option
 
   let systemName : string = "Dynamic Z Tree Aggregation Protocol"
 
@@ -73,13 +73,13 @@ module ZTreeAggregationArrangement (P : Params) = struct
     fun n s ->
       Obj.magic (coq_ZTreeAggregation_MultiParams.input_handlers (Obj.magic n) (Obj.magic SendAggregate) (Obj.magic s))
 
-  let setSendAggregateTimeout : timeout_setter = fun n s -> P.aggregate_timeout
+  let setSendAggregateTimeout : timeout_setter = fun n s -> Some P.aggregate_timeout
 
   let deliverBroadcastHandler : task_handler =
     fun n s ->
       Obj.magic (coq_ZTreeAggregation_MultiParams.input_handlers (Obj.magic n) (Obj.magic Broadcast) (Obj.magic s))
 
-  let setBroadcastTimeout : timeout_setter = fun n s -> P.broadcast_timeout
+  let setBroadcastTimeout : timeout_setter = fun n s -> Some P.broadcast_timeout
 
   let timeoutTasks : (task_handler * timeout_setter) list = 
     [
diff --git a/extraction/zaggregation-dynamic/test/OptsTest.ml b/extraction/zaggregation-dynamic/test/OptsTest.ml
@@ -1,6 +1,6 @@
 open OUnit2
 open ListLabels
-open TestCommon
+open Util
 
 let tear_down () text_ctxt =
   Opts.cluster := Opts.cluster_default;
diff --git a/extraction/zaggregation-dynamic/test/TestCommon.ml b/extraction/zaggregation-dynamic/test/TestCommon.ml
