Commit ba79642d authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge with latest changes rom master

parents 647571c5 123de65a
......@@ -67,14 +67,15 @@ Proof.
intros. cbn in *; congruence. }
exists Gamma; intros approxEnv_E1E2.
destruct subdivs.
- edestruct result_checking_sound; eauto.
intuition.
- edestruct result_checking_sound as ((outVars & Hssa) & validR & validErr & validFPR); eauto.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single; eauto.
destruct H5 as (? & ? & ?).
edestruct validErrorBoundsRec_single as ((vFP & mFP & eval_fp_e) & ?); eauto.
repeat eexists; eauto.
- (* general version of subdivs_checking_sound *) admit.
Admitted.
- edestruct subdivs_checking_sound as ((outVars & Hssa) & validR & validErr & validFPR); eauto.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single as ((vFP & mFP & eval_fp_e) & ?); eauto.
repeat eexists; eauto.
Qed.
(**
Soundness proof for the certificate checker.
......
......@@ -3074,8 +3074,8 @@ Proof.
- apply validErrorboundAA_sound_binop; auto.
- apply validErrorboundAA_sound_fma; auto.
- apply validErrorboundAA_sound_downcast; auto.
- (*FIXME *)
Qed.
- admit.
Abort.
Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map:
(forall e' : FloverMap.key,
......@@ -3200,7 +3200,12 @@ Proof.
end.
cbn in Hiv.
now rewrite Rabs_Rle_condition.
<<<<<<< HEAD
- (* FIXME *)
=======
- admit.
Abort.
>>>>>>> master
(*
Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map :=
......@@ -3817,4 +3822,4 @@ Proof.
cbn in H12.
now rewrite Rabs_Rle_condition.
Qed.
*)
\ No newline at end of file
*)
......@@ -26,11 +26,10 @@ Theorem result_checking_sound (e: expr Q) (absenv: analysisResult) P Qmap defVar
unsat_queries Qmap ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
ResultChecker e absenv P Qmap defVars Gamma = true ->
exists outVars,
ssa e (freeVars e) outVars /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(exists outVars, ssa e (freeVars e) outVars) /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -56,7 +55,7 @@ Proof.
assert (NatSet.Subset (freeVars e -- NatSet.empty) (freeVars e)).
{ hnf; intros a in_empty.
set_tac. }
rename R into validFPRanges.
rename R into validFPR.
rename R0 into validRoundoffErr.
pose proof (validSSA_checks_freeVars _ _ L) as sub.
destruct (validSSA_sound e (preVars P)) as [outVars ssa_e]; auto.
......@@ -108,7 +107,7 @@ Corollary result_checking_sound_single (e: expr Q) (absenv: analysisResult) P Qm
Proof.
intros * deltas_matched P_valid unsat_qs valid_typeMap results_valid.
exists Gamma; intros approxE1E2.
edestruct result_checking_sound as (? & _ & validRange & Hsound & _); try eauto.
edestruct result_checking_sound as (_ & validRange & Hsound & _); try eauto.
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBoundsRec_single in Hsound; eauto.
......
......@@ -9,8 +9,24 @@ Require Import List FunInd Sorting.Permutation Sorting.Mergesort Orders.
Fixpoint resultLeq e (A1 A2: analysisResult) :=
match e with
| Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2
| Binop b e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 &&
match b with
| Div => match FloverMap.find e2 A2 with
| Some (iv2, err) =>
Qleb 0 err &&
(Qleb (snd iv2 + err) 0 && negb (Qeq_bool (snd iv2 + err) 0)
|| Qleb 0 (fst iv2 - err) && negb (Qeq_bool (fst iv2 - err) 0))
| _ => false
end
| _ => true
end
| Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2
| Let _ x e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 &&
match FloverMap.find (Var Q x) A2, FloverMap.find e1 A2 with
| Some (ivX, errX), Some (iv1, err1) =>
Qeqb (ivlo iv1) (ivlo ivX) && Qeqb (ivhi iv1) (ivhi ivX) && Qeqb err1 errX
| _, _ => false
end
| _ => true
end &&
match FloverMap.find e A1, FloverMap.find e A2 with
......@@ -40,6 +56,218 @@ Proof.
- apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
Qed.
Lemma resultLeq_range_sound e A1 A2 E Gamma :
resultLeq e A1 A2 = true ->
validRanges e A1 E Gamma ->
validRanges e A2 E Gamma.
Proof.
induction e in E |- *; cbn.
- intros Hleq (_ & iv & err & vR & Hfind & Heval & Hiv).
rewrite Hfind in Hleq. Flover_compute.
split; auto. kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra.
- intros Hleq (_ & iv & err & vR & Hfind & Heval & Hiv).
rewrite Hfind in Hleq. Flover_compute.
split; auto. kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra.
- intros H (H1 & iv & err & vR & Hfind & Heval & Hiv).
apply andb_true_iff in H as [Hleq1 Hleq].
rewrite Hfind in Hleq. Flover_compute.
split; auto. kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra.
- intros H ((_ & H1 & H2) & iv & err & vR & Hfind & Heval & Hiv).
apply andb_true_iff in H as [H Hleq].
apply andb_true_iff in H as [H Hdiv].
apply andb_true_iff in H as [Hleq1 Hleq2].
rewrite Hfind in Hleq.
(* destruct (FloverMap.find (Binop b e1 e2) A2) eqn: Hfind2; try congruence. *)
repeat split; auto.
+ intros -> ivA2 errA2 Hfind2.
edestruct (resultLeq_sound _ _ _ Hleq2)
as (ivA1 & errA1 & ? & ? & Hfind1 & Hfind2' & Hsub & _).
rewrite Hfind2' in Hfind2.
injection Hfind2. intros -> ->.
(* specialize (Hdiv eq_refl ivA1 errA1 Hfind1). *)
apply andb_true_iff in Hsub as [Hsub1 Hsub2].
cbn in *.
unfold error in *.
rewrite Hfind2' in Hdiv.
apply orb_true_iff.
apply andb_true_iff in Hdiv as [Herr Hdiv].
apply orb_true_iff in Hdiv as [Hdiv | Hdiv]; [left | right].
* apply andb_true_iff in Hdiv as [Hle Hneq].
apply andb_true_iff.
apply Qle_bool_iff in Herr.
apply Qle_bool_iff in Hle.
split; [apply Qle_bool_iff; lra |].
destruct (Qeq_bool (snd ivA2) 0) eqn: H; auto.
apply Qeq_bool_iff in H.
assert (snd ivA2 + errA2 == 0) as Heq by lra.
apply Qeq_bool_iff in Heq.
now rewrite Heq in Hneq.
* apply andb_true_iff in Hdiv as [Hle Hneq].
apply andb_true_iff.
apply Qle_bool_iff in Herr.
apply Qle_bool_iff in Hle.
split; [apply Qle_bool_iff; lra |].
destruct (Qeq_bool (fst ivA2) 0) eqn: H; auto.
apply Qeq_bool_iff in H.
assert (fst ivA2 - errA2 == 0) as Heq by lra.
apply Qeq_bool_iff in Heq.
now rewrite Heq in Hneq.
+ destruct (FloverMap.find (Binop b e1 e2) A2) as [[iv2 err2]|] eqn: Hfind2; try congruence.
kill_trivial_exists. exists vR.
apply andb_true_iff in Hleq as [Hsub _].
apply andb_true_iff in Hsub as [Hsub1 Hsub2].
canonize_hyps; cbn in *.
repeat split; auto; lra.
- intros H ((H1 & H2 & H3) & iv & err & vR & Hfind & Heval & Hiv).
apply andb_true_iff in H as [H Hleq].
apply andb_true_iff in H as [H Hleq3].
apply andb_true_iff in H as [Hleq1 Hleq2].
rewrite Hfind in Hleq. Flover_compute.
split; auto. kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra.
- intros H (H1 & iv & err & vR & Hfind & Heval & Hiv).
apply andb_true_iff in H as [Hleq1 Hleq].
rewrite Hfind in Hleq. Flover_compute.
split; auto. kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra.
- intros H ((H1 & Hx & H2) & iv & err & vR & Hfind & Heval & Hiv).
apply andb_true_iff in H as [H Hleq].
apply andb_true_iff in H as [Hleq1 Hleq2].
rewrite Hfind in Hleq. Flover_compute.
repeat split; auto.
+ repeat eexists. repeat split; eauto.
unfold Qeqb in *.
now rewrite L1, R2.
+ kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra.
Qed.
Lemma resultLeq_error_sound e A1 A2 E1 E2 Gamma :
resultLeq e A1 A2 = true ->
validErrorBounds e E1 E2 A1 Gamma ->
validErrorBounds e E1 E2 A2 Gamma.
Proof.
intros Hleq err_sound DeltaMap delta_sound.
specialize (err_sound _ delta_sound).
revert E1 E2 err_sound.
induction e; intros E1 E2 err_sound; cbn.
- split; auto. intros vR iv err Heval Hfind.
cbn in Hleq.
Flover_compute.
unfold error in *.
assert (e0 = err) by congruence; subst.
edestruct err_sound as (_ & H1 & H2); eauto.
split; auto.
canonize_hyps.
intros vFP mFP HevalFP.
specialize (H2 vFP mFP HevalFP).
lra.
- split; auto. intros vR iv err Heval Hfind.
cbn in Hleq.
Flover_compute.
unfold error in *.
assert (e0 = err) by congruence; subst.
edestruct err_sound as (_ & H1 & H2); eauto.
split; auto.
canonize_hyps.
intros vFP mFP HevalFP.
specialize (H2 vFP mFP HevalFP).
lra.
- edestruct err_sound as [H1 Herr].
cbn in Hleq.
apply andb_true_iff in Hleq as [Hleq1 Hleq].
split; [destruct u; auto |].
intros vR iv err Heval Hfind.
Flover_compute.
unfold error in *.
assert (e1 = err) by congruence; subst.
edestruct Herr as [Hex Hall]; eauto.
split; auto.
canonize_hyps.
intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP).
lra.
- edestruct err_sound as ((_ & H1 & H2) & Herr).
cbn in Hleq.
apply andb_true_iff in Hleq as [H Hleq].
apply andb_true_iff in H as [H Hdiv].
apply andb_true_iff in H as [Hleq1 Hleq2].
split.
+ repeat split; auto.
intros -> iv2 err Hfind2.
unfold error in *.
rewrite Hfind2 in Hdiv.
now apply andb_true_iff in Hdiv as [_ Hdiv].
+ intros vR iv err Heval Hfind.
clear Hdiv.
Flover_compute.
unfold error in *.
assert (e0 = err) by congruence; subst.
edestruct Herr as [Hex Hall]; eauto.
split; auto.
canonize_hyps.
intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP).
lra.
- edestruct err_sound as ((H1 & H2 & H3) & Herr).
cbn in Hleq.
apply andb_true_iff in Hleq as [H Hleq].
apply andb_true_iff in H as [H Hleq3].
apply andb_true_iff in H as [Hleq1 Hleq2].
split; auto.
intros vR iv err Heval Hfind.
Flover_compute.
unfold error in *.
assert (e0 = err) by congruence; subst.
edestruct Herr as [Hex Hall]; eauto.
split; auto.
canonize_hyps.
intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP).
lra.
- edestruct err_sound as [H1 Herr].
cbn in Hleq.
apply andb_true_iff in Hleq as [Hleq1 Hleq].
split; auto.
intros vR iv err Heval Hfind.
Flover_compute.
unfold error in *.
assert (e1 = err) by congruence; subst.
edestruct Herr as [Hex Hall]; eauto.
split; auto.
canonize_hyps.
intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP).
lra.
- edestruct err_sound as ((H1 & _ & H2) & Herr).
cbn in Hleq.
apply andb_true_iff in Hleq as [H Hleq].
apply andb_true_iff in H as [H Hx].
apply andb_true_iff in H as [Hleq1 Hleq2].
split; auto.
+ split; auto. split; auto.
intros iv1 err1 ivX errX Hfind1 HfindX.
unfold error in *.
rewrite Hfind1, HfindX in Hx.
apply andb_true_iff in Hx as [Hx Hxerr].
apply andb_true_iff in Hx as [Hx1 Hx2].
unfold Qeqb in *.
canonize_hyps. now repeat split.
+ intros vR iv err Heval Hfind.
Flover_compute.
unfold error in *.
assert (e0 = err) by congruence; subst.
edestruct Herr as [Hex Hall]; eauto.
split; auto.
canonize_hyps.
intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP).
lra.
Qed.
(* TODO: maybe put this somewhere else *)
Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
NatSet.Empty dVars ->
......@@ -438,10 +666,16 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs de
forall (E1 E2: env) DeltaMap,
(forall (e': R) (m': mType),
exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
eval_precond E1 P ->
(forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
SubdivsChecker e absenv P subdivs defVars Gamma = true ->
(exists outVars, ssa e (freeVars e) outVars) /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(*
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
exists iv err vR vF m,
......@@ -451,8 +685,9 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs de
(forall vF m,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
*)
Proof.
intros * deltas_matched P_valid unsat_qs valid_typeMap chk.
intros * deltas_matched approxEnv P_valid unsat_qs valid_typeMap chk.
apply andb_prop in chk as [chk valid_subdivs].
apply andb_prop in chk as [valid_ssa valid_cover].
eapply (checkPreconds_sound) in P_valid as [P1 [in_subdivs P_valid]]; eauto.
......@@ -463,14 +698,21 @@ Proof.
pose proof (checkSubdivs_sound e _ _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P1 Qmap defVars Gamma = true) as res_check
by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
eapply approxEnv_empty_dVars in approxEnv; eauto.
edestruct result_checking_sound as (Hssa & validR & validErr & validFPR); eauto.
{ apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
repeat split; eauto using resultLeq_range_sound, resultLeq_error_sound.
Qed.
(*
exists Gamma; intros approxE1E2.
assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
by (eapply approxEnv_empty_dVars; eauto).
assert (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
{ eapply result_checking_sound; eauto.
{ edestruct result_checking_sound; eauto; [| intuition].
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
assert (validErrorBounds e E1 E2 A Gamma) as Hsound.
{ eapply result_checking_sound; eauto.
{ edestruct result_checking_sound; eauto; [| intuition].
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
......@@ -485,3 +727,4 @@ Proof.
specialize (err_bounded vF0 m Heval).
lra.
Qed.
*)
......@@ -462,4 +462,4 @@ Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_det_ignore_bind2; [eauto |].
edestruct ssa_inv_let; eauto.
Qed
Qed.
Subproject commit 78f69d7fcdd795890f213134d66582ece116e14b
Subproject commit 7acebe9f434d9882401f73a0d4a14e9e5e4844a8
......@@ -11,8 +11,19 @@
# #
##############################################################################
TIMECMD=""
PROVERS=(coq hol4 binary)
unameOut="$(uname -s)"
case "${unameOut}" in
Linux*) TIMECMD=/usr/bin/time;;
Darwin*) TIMECMD=/usr/local/bin/time;;
# CYGWIN*) machine=Cygwin;;
# MINGW*) machine=MinGw;;
# *) machine="UNKNOWN:${unameOut}"
esac
#PROVERS=(coq hol4 binary)
PROVERS=(coq)
arr=()
while IFS= read -r -d $'\0'; do
......@@ -24,10 +35,13 @@ DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_fixed_$DATE
echo "Creating HOL4 heap for evaluation" >>$2
cd ./hol4/output/
Holmake heap >>$2
cd ../../
#echo "Creating HOL4 heap for evaluation" >>$2
#cd ./hol4/output/
#Holmake heap >>$2
#cd ../../
#echo "Daisy Coq, Daisy HOL4, Daisy Binary, Coq1, Coq2, Coq3, HOL4_1, HOL4_2, HOL4_3, CakeML1, CakeML2, CakeML3, Coqbin1, Coqbin2, Coqbin3" >>$1
echo "Daisy Coq, Coq1, Coq2, Coq3" >>$1
for file in "${arr[@]}"
do
......@@ -43,10 +57,13 @@ do
cd ./daisy
for prv in "${PROVERS[@]}"
do
RESULT=$( { /usr/bin/time -f ", %e" \
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--precision=Fixed32 \
--rangeMethod=smt \
--errorMethod=interval \
--divLimit=5 \
--totalOpt=150 \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1 )
......@@ -59,80 +76,81 @@ 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
#run HOL4 checker 3 times
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=${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=${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=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
cd ../../
#run HOL4 binary 3 times
echo "Working on CakeML $CERTNAME"
RESULT=$( { /usr/bin/time -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 \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
# #run Coq binary 3 times
echo "Working on Coq binary $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo $RESULT >>$1
# #run HOL4 checker 3 times
# 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=${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=${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=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# cd ../../
#
# #run HOL4 binary 3 times
# echo "Working on CakeML $CERTNAME"
# RESULT=$( { /usr/bin/time -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 \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# # #run Coq binary 3 times
# echo "Working on Coq binary $CERTNAME"
# RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo -n $RESULT >>$1
#
# RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo -n $RESULT >>$1
#
# RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo $RESULT >>$1
echo "" >>$1
mv ./daisy/output/certificate_* /tmp/artifact_fixed_$DATE/
done
......@@ -65,8 +65,8 @@ do
--rangeMethod=smt \
--errorMethod=interval \
--subdiv \
--divLimit=3 \
--totalOpt=100 \
--divLimit=5 \
--totalOpt=150 \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1 )
......@@ -81,8 +81,8 @@ do
--rangeMethod=smt \
--errorMethod=interval \