Merge branch 'master' into errors_affine

.gitmodules

 [submodule "hol4/cakeml"]
-	branch = master
+	branch = FMA_support
 	path = hol4/cakeml
 	url = https://github.com/CakeML/cakeml.git
 

Dockerfile

-FROM debian:latest
+FROM ocaml/opam2:latest
 
 WORKDIR /root
 
+USER root
+
 #Necessary packages for opam
 RUN apt-get update && \
-    apt-get install -y build-essential aspcud m4 wget unzip git
+    apt-get install -y build-essential aspcud m4 wget unzip git curl
 
-# Install opam
-RUN wget https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh -O - | sh -s /usr/local/bin
+# # Configure opam
+# RUN opam init --comp=4.05.0 --auto-setup && \
+RUN eval `opam config env`
 
-# Configure opam
-RUN opam init --comp=4.05.0 --auto-setup && \
-    eval `opam config env`
+RUN cd /home/opam/opam-repository && git pull && cd
 
 # Install coq and dependencies
-RUN opam repo add coq-released https://coq.inria.fr/opam/released && \
+RUN opam repo add coq-released https://coq.inria.fr/opam/released --set-default && \
     opam update
 
 #Install coq 8.7.2 in a switch
-RUN opam switch -A 4.05.0 coq8.7.2
+RUN opam switch create coq8.7.2 ocaml-base-compiler.4.05.0 && \
+    eval `opam config env`
+
 RUN opam install coq.8.7.2 coq-flocq.2.6.1
 
 #Install coq 8.8 in a switch
-RUN opam switch -A 4.05.0 coq8.8
-RUN opam install coq.8.8.0 coq-flocq.2.6.1
+RUN opam switch create coq8.8 ocaml-base-compiler.4.05.0
+RUN opam install coq.8.8.2 coq-flocq.2.6.1
 
 # Install polyml from git
 RUN git clone https://github.com/polyml/polyml.git polyml && \

coq/configure_coq.sh

@@ -28,8 +28,12 @@ case "$coq_ver" in
     ;;
     8.8.0)
     ;;
+    8.8.1)
+    ;;
+    8.8.2)
+    ;;
     *)
-        echo "Error: Need 8.7.2"
+        echo "Error: Need one of Coq 8.7.2, 8.8.0 8.8.1 or 8.8.2"
         exit 1
 esac
 

hol4/.HOLCOMMIT

-f243fe78da5dcc426046ce1b6a0f756e6aa524b9
+7f7650b1f7d9fbc79f55646dabcf225b5cf0fff4

hol4/CertificateGeneratorScript.sml

+open RealIntervalInferenceTheory ErrorIntervalInferenceTheory ExpressionsTheory
+     FloverMapTheory TypeValidatorTheory CommandsTheory AbbrevsTheory
+     ExpressionAbbrevsTheory;
+open preamble;
+
+val _ = new_theory "CertificateGenerator";
+
+val CertificateGeneratorExp_def = Define `
+  CertificateGeneratorExp (f:real expr) (P:precond) (Gamma:typeMap)
+    :(real expr # precond # typeMap # analysisResult) option =
+    let
+      ivMap = inferIntervalbounds f P FloverMapTree_empty;
+      fullTMap = getValidMap Gamma f FloverMapTree_empty;
+    in
+      case ivMap, fullTMap of
+      | SOME ivMap, Succes tMap =>
+        (case inferErrorbound f tMap ivMap FloverMapTree_empty of
+        | SOME errMap => SOME (f,P,Gamma,errMap)
+        | NONE => NONE)
+      | _, _ => NONE`;
+
+val getExp_def = Define `
+  getExp (f, P, Gamma, errMap) = f`;
+
+val getError_def = Define `
+  getError (f, P, Gamma, errMap) = FloverMapTree_find f errMap`;
+
+val CertificateGeneratorCmd_def = Define `
+  CertificateGeneratorCmd (f:real cmd) (P:precond) (Gamma:typeMap)
+    :(real cmd # precond # typeMap # analysisResult) option =
+    let
+      ivMap = inferIntervalboundsCmd f P FloverMapTree_empty;
+      fullTMap = getValidMapCmd Gamma f FloverMapTree_empty;
+    in
+      case ivMap, fullTMap of
+      | SOME ivMap, Succes tMap =>
+        (case inferErrorboundCmd f tMap ivMap FloverMapTree_empty of
+        | SOME errMap => SOME (f,P,Gamma,errMap)
+        | NONE => NONE)
+      | _, _ => NONE`;
+
+val getCmd_def = Define `
+  getCmd (f, P, Gamma, errMap) = f`;
+
+val getError_def = Define `
+  getError (f, P, Gamma, errMap) = FloverMapTree_find (getRetExp f) errMap`;
+
+val _ = export_theory ();

hol4/ErrorIntervalInferenceScript.sml

+ (**
+   This file contains the HOL4 implementation of the error bound validator as well
+   as its soundness proof. The function validErrorbound is the Error bound
+   validator from the certificate checking process. Under the assumption that a
+   valid range arithmetic result has been computed, it can validate error bounds
+   encoded in the analysis result. The validator is used in the file
+   CertificateChecker.v to build the complete checker.
+ **)
+open simpLib realTheory realLib RealArith pred_setTheory;
+open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
+     RealRangeArithTheory FloverTactics MachineTypeTheory
+     ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
+     TypeValidatorTheory IntervalValidationTheory EnvironmentsTheory
+     RealIntervalInferenceTheory
+     CommandsTheory ssaPrgsTheory FloverMapTheory;
+open preamble;
+
+val _ = new_theory "ErrorIntervalInference";
+
+val inferErrorbound_def = Define `
+  inferErrorbound e (typeMap: typeMap) (I:ivMap) (akk:analysisResult) :analysisResult option=
+  (case (FloverMapTree_find e akk) of
+  | SOME _ => SOME akk
+  | NONE =>
+    do
+      iv_f <- FloverMapTree_find e I;
+      m <- FloverMapTree_find e typeMap;
+      (case e of
+      | Var v =>
+        SOME (FloverMapTree_insert e (iv_f, computeError (maxAbs iv_f) m) akk)
+      | Const _ n =>
+        SOME (FloverMapTree_insert e (iv_f, computeError (maxAbs iv_f) m) akk)
+      | Unop Neg e1 =>
+        do
+        recRes <- inferErrorbound e1 typeMap I akk;
+        (iv, err1) <- FloverMapTree_find e1 recRes;
+        SOME (FloverMapTree_insert e (iv_f, err1) recRes);
+        od
+      | Unop Inv e1 => NONE
+      | Binop op e1 e2 =>
+        do
+        recRes1 <- inferErrorbound e1 typeMap I akk;
+        recRes2 <- inferErrorbound e2 typeMap I recRes1;
+        (ive1, err1) <- FloverMapTree_find e1 recRes2;
+        (ive2, err2) <- FloverMapTree_find e2 recRes2;
+          let errIve1 = widenInterval ive1 err1 in
+          let errIve2 = widenInterval ive2 err2 in
+          let upperBoundE1 = maxAbs ive1 in
+          let upperBoundE2 = maxAbs ive2 in
+          if ((op = Div /\ noDivzero (IVhi errIve2) (IVlo errIve2) \/ op <> Div))
+          then
+            let eNew =
+              (case op of
+               | Plus =>
+                 let mAbs = maxAbs (addInterval errIve1 errIve2) in
+                   err1 + err2 + computeError mAbs m
+               | Sub =>
+                 let mAbs = maxAbs (subtractInterval errIve1 errIve2) in
+                   err1 + err2 + computeError mAbs m
+               | Mult =>
+                 let mAbs = maxAbs (multInterval errIve1 errIve2);
+                     eProp = upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2 in
+                   eProp + computeError mAbs m
+               | Div =>
+                 let upperBoundInvE2 = maxAbs (invertInterval ive2);
+                  minAbsIve2 = minAbsFun (errIve2);
+                  errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2;
+                  mAbs = maxAbs (divideInterval errIve1 errIve2);
+                  eProp = upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv in
+                  eProp + computeError mAbs m)
+            in
+            SOME (FloverMapTree_insert e (iv_f, eNew) recRes2)
+          else NONE;
+        od
+      | Fma e1 e2 e3 =>
+        do
+        recRes1 <- inferErrorbound e1 typeMap I akk;
+        recRes2 <- inferErrorbound e2 typeMap I recRes1;
+        recRes3 <- inferErrorbound e3 typeMap I recRes2;
+        (ive1, err1) <- FloverMapTree_find e1 recRes3;
+        (ive2, err2) <- FloverMapTree_find e2 recRes3;
+        (ive3, err3) <- FloverMapTree_find e3 recRes3;
+          let errIve1 = widenInterval ive1 err1;
+              errIve2 = widenInterval ive2 err2;
+              errIve3 = widenInterval ive3 err3;
+              upperBoundE1 = maxAbs ive1;
+              upperBoundE2 = maxAbs ive2;
+              upperBoundE3 = maxAbs ive3;
+              errIntv_prod = multInterval errIve2 errIve3;
+              mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3);
+              mAbs = maxAbs (addInterval errIve1 errIntv_prod);
+              eNew = err1 + mult_error_bound + computeError mAbs m
+          in
+          SOME (FloverMapTree_insert e (iv_f, eNew) recRes3);
+        od
+      | Downcast m1 e1 =>
+        do
+        recRes <- inferErrorbound e1 typeMap I akk;
+        (ive1, err1) <- FloverMapTree_find e1 recRes;
+          let errIve1 = widenInterval ive1 err1;
+              mAbs = maxAbs errIve1;
+              eNew = err1 + computeError mAbs m1;
+          in
+          SOME (FloverMapTree_insert e (iv_f, eNew) recRes)
+        od)
+    od)`;
+
+val inferErrorboundCmd_def = Define `
+  inferErrorboundCmd (f:real cmd) (typeMap: (real expr # mType) binTree)
+                    (I:ivMap) (akk:analysisResult) =
+    case f of
+      | Let m x e g  =>
+        do
+          recRes <- inferErrorbound e typeMap I akk;
+          (ive, erre) <- FloverMapTree_find e recRes;
+          inferErrorboundCmd g typeMap I (FloverMapTree_insert (Var x) (ive, erre) recRes);
+        od
+      | Ret e =>
+        inferErrorbound e typeMap I akk`;
+
+val _ = export_theory();

hol4/Infra/FloverTactics.sml

@@ -128,6 +128,8 @@ let val (name, list) = dest_type t in
      | _ => (num, rev lst)
 end
 
+exception ERR of string;
+
 fun getPatTerm t =
   let
       val decl_list = decls (term_to_string t);
@@ -146,7 +148,7 @@ fun getPatTerm t =
                            (mk_comb (t, var), tl tyList)
                        end)
           end
-      else raise ERR "Too many constants" ""
+      else raise ERR "Too many constants"
 end;
 
 (* This variable is supposed to hold all defined functions *)

hol4/RealIntervalInferenceScript.sml

+(**
+    Interval arithmetic checker and its soundness proof.
+    The function validIntervalbounds checks wether the given analysis result is
+    a valid range arithmetic for each sub term of the given exprression e.
+    The computation is done using our formalized interval arithmetic.
+    The function is used in CertificateChecker.v to build the full checker.
+**)
+open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
+     sptreeLib;
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
+     ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
+     MachineTypeTheory FloverMapTheory TypeValidatorTheory RealRangeArithTheory
+     ExpressionSemanticsTheory;
+open preamble;
+
+val _ = new_theory "RealIntervalInference";
+
+val _ = monadsyntax.enable_monadsyntax();
+val _ = List.app monadsyntax.enable_monad ["option"];
+val _ = type_abbrev ("ivMap", ``:(real # real) fMap``);
+
+val inferIntervalbounds_def = Define `
+  inferIntervalbounds f (P:precond) (akk:ivMap) :ivMap option =
+  (case (FloverMapTree_find f akk) of
+    | SOME intv => SOME akk
+    | NONE =>
+      (case f of
+        | Var v =>
+          SOME (FloverMapTree_insert f (P v) akk)
+        | Const m n =>
+          SOME (FloverMapTree_insert f (n,n) akk)
+        | Unop op f1 =>
+          do
+            recRes <- inferIntervalbounds f1 P akk;
+            iv_f1 <- FloverMapTree_find f1 recRes;
+              case op of
+                | Neg =>
+                  SOME (FloverMapTree_insert f (negateInterval iv_f1) recRes)
+                | _ => NONE
+          od
+        | Downcast m f1 =>
+          do
+            recRes <- inferIntervalbounds f1 P akk;
+            iv_f1 <- FloverMapTree_find f1 recRes;
+            SOME (FloverMapTree_insert f iv_f1 recRes);
+          od
+        | Binop op f1 f2 =>
+          do
+            recRes1 <- inferIntervalbounds f1 P akk;
+            recRes2 <- inferIntervalbounds f2 P recRes1;
+            iv_f1 <- FloverMapTree_find f1 recRes2;
+            iv_f2 <- FloverMapTree_find f2 recRes2;
+            if (op = Div /\ (IVlo iv_f2 <= 0 /\ 0 <= IVhi iv_f2))
+            then NONE
+            else
+              SOME
+                (let new_iv =
+                  (case op of
+                    | Plus => addInterval iv_f1 iv_f2
+                    | Sub => subtractInterval iv_f1 iv_f2
+                    | Mult => multInterval iv_f1 iv_f2
+                    | Div => divideInterval iv_f1 iv_f2)
+                  in FloverMapTree_insert f new_iv recRes2);
+            od
+        | Fma f1 f2 f3 =>
+          do
+            recRes1 <- inferIntervalbounds f1 P akk;
+            recRes2 <- inferIntervalbounds f2 P recRes1;
+            recRes3 <- inferIntervalbounds f3 P recRes2;
+            iv_f1 <- FloverMapTree_find f1 recRes3;
+            iv_f2 <- FloverMapTree_find f2 recRes3;
+            iv_f3 <- FloverMapTree_find f3 recRes3;
+            SOME (FloverMapTree_insert f (addInterval iv_f1 (multInterval iv_f2 iv_f3)) recRes3);
+          od))`;
+
+val inferIntervalboundsCmd_def = Define `
+  inferIntervalboundsCmd (f:real cmd) (P:precond) (akk:ivMap) :ivMap option =
+    case f of
+     | Let m x e g =>
+      do
+        recRes <- inferIntervalbounds e P akk;
+        iv_x <- FloverMapTree_find e recRes;
+        inferIntervalboundsCmd g P (FloverMapTree_insert (Var x) iv_x recRes);
+      od
+   | Ret e => inferIntervalbounds e P akk`;
+
+val _ = export_theory();

cakeml @ 401ed36d

-Subproject commit 993321ec18c82a08de25de644745215d5ec3fc28
+Subproject commit 401ed36dc008523f906716c7d93711c39edec3d5

scripts/eval_interval.sh

@@ -11,6 +11,16 @@
 #                                                                            #
 ##############################################################################
 
+TIMECMD=""
+
+unameOut="$(uname -s)"
+case "${unameOut}" in
+    Linux*)     TIMECMD=/usr/bin/time;;
+    Darwin*)    machine=/usr/local/bin/time;;
+    # CYGWIN*)    machine=Cygwin;;
+    # MINGW*)     machine=MinGw;;
+    # *)          machine="UNKNOWN:${unameOut}"
+esac
 
 PROVERS=(coq hol4 binary)
 
@@ -48,7 +58,7 @@ do
       echo "Doing single precision eval for $FILENAME" >>$2
       for prv in "${PROVERS[@]}"
       do
-          RESULT=$( { /usr/bin/time -f ", %e" \
+          RESULT=$( { $TIMECMD -f ", %e" \
                                     ./daisy $FILEPATH --certificate=$prv \
                                     --errorMethod=interval \
                                     --results-csv=$FILENAME.csv \
@@ -60,7 +70,7 @@ do
       echo "Doing mixed-precision eval for $FILENAME" >>$2
       for prv in "${PROVERS[@]}"
       do
-          RESULT=$( { /usr/bin/time -f ", %e" \
+          RESULT=$( { $TIMECMD -f ", %e" \
                                     ./daisy $FILEPATH --certificate=$prv \
                                     --errorMethod=interval \
                                     --mixed-precision=testcases/daisy-mixed-precision-maps/$PMAP \
@@ -77,19 +87,19 @@ do
 
   #run coq checker 3 times
   echo "Working on Coq $CERTNAME" >>$2
-  RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
+  RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
                             ./daisy/output/$CERTNAME.v; } 2>&1)
   echo -n $RESULT >>$1
   rm ./daisy/output/$CERTNAME.vo
   rm ./daisy/output/$CERTNAME.glob
 
-  RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
+  RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
                             ./daisy/output/$CERTNAME.v; } 2>&1)
   echo -n $RESULT >>$1
   rm ./daisy/output/$CERTNAME.vo
   rm ./daisy/output/$CERTNAME.glob
 
-  RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
+  RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
                             ./daisy/output/$CERTNAME.v; } 2>&1)
   echo -n $RESULT >>$1
 
@@ -97,21 +107,21 @@ do
   cp ./daisy/output/*Script.sml ./hol4/output/
   cd ./hol4/output/
   echo "Working on $CERTNAME Theory.sig" >>$2
-  RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
+  RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
   RESULT=${RESULT#*M1}
   RESULT=${RESULT%%M2*}
   echo -n $RESULT >>$1
 
   rm ./certificate_*Theory*
 
-  RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
+  RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
   RESULT=${RESULT#*M1}
   RESULT=${RESULT%%M2*}
   echo -n $RESULT >>$1
 
   rm ./certificate_*Theory*
 
-  RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
+  RESULT=$( { $TIMECMD -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
   RESULT=${RESULT#*M1}
   RESULT=${RESULT%%M2*}
   echo -n $RESULT >>$1
@@ -121,31 +131,31 @@ do
 
   #run HOL4 binary 3 times
   echo "Working on CakeML $CERTNAME"
-  RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
+  RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
                             ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
   echo -n $RESULT >>$1
 
-  RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
+  RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
                             ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
   echo -n $RESULT >>$1
 
-  RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
+  RESULT=$( { $TIMECMD -f ", %e" hol4/binary/cake_checker \
                             ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
   echo -n $RESULT >>$1
 
   # #run Coq binary
   echo "Working on Coq binary $CERTNAME"
-  RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
+  RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
                             ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
 
   echo $RESULT >>$1
 
-  RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
+  RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
                             ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
 
   echo $RESULT >>$1
 
-  RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
+  RESULT=$( { $TIMECMD -f ", %e" coq/binary/coq_checker_native \
                             ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
 
   echo $RESULT >>$1