From faa512c74ba61811153e5d7d69cc9be570a8def8 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Sun, 12 May 2019 18:41:18 +0200 Subject: [PATCH 1/4] Add support for 64-bit floating-point translation for binary and unary ops --- translator/ml_translatorLib.sml | 18 ++++- translator/ml_translatorScript.sml | 91 ++++++++++++++++++++++++- translator/ml_translator_testScript.sml | 6 ++ 3 files changed, 111 insertions(+), 4 deletions(-) diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index 3e02cbe300..607b1b4f2b 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -419,9 +419,9 @@ val basic_theories = ["alist", "arithmetic", "bag", "bitstring", "bit", "bool", "combin", "container", "divides", "fcp", "finite_map", "float", "fmaptree", "frac", "gcdset", "gcd", "ind_type", "integer_word", - "integer", "integral", "list", "llist", "marker", "measure", - "numeral_bit", "numeral", "numpair", "numposrep", "num", "one", - "operator", "option", "pair", "path", "patricia_casts", + "integer", "integral", "list", "llist", "marker", "machine_iee", + "measure", "numeral_bit", "numeral", "numpair", "numposrep", "num", + "one", "operator", "option", "pair", "path", "patricia_casts", "patricia", "poly", "poset", "powser", "pred_set", "prelim", "prim_rec", "quote", "quotient_list", "quotient_option", "quotient_pair", "quotient_pred_set", "quotient_sum", "quotient", @@ -2708,6 +2708,15 @@ val builtin_binops = Eval_INT_LESS_EQ, Eval_INT_GREATER, Eval_INT_GREATER_EQ, + Eval_FLOAT_ADD, + Eval_FLOAT_SUB, + Eval_FLOAT_MULT, + Eval_FLOAT_DIV, + Eval_FLOAT_LESS, + Eval_FLOAT_LESS_EQ, + Eval_FLOAT_GREATER, + Eval_FLOAT_GREATER_EQ, + Eval_FLOAT_EQ, Eval_force_gc_to_run, Eval_force_unit_type, Eval_strsub, @@ -2728,6 +2737,9 @@ val builtin_monops = Eval_vector, Eval_int_of_num, Eval_num_of_int, + Eval_FLOAT_ABS, + Eval_FLOAT_SQRT, + Eval_FLOAT_NEG, Eval_empty_ffi, Eval_force_out_of_memory_error, Eval_Chr, diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml index 451aaa3f73..eb6ff3c7cc 100644 --- a/translator/ml_translatorScript.sml +++ b/translator/ml_translatorScript.sml @@ -5,7 +5,8 @@ *) open integerTheory ml_progTheory astTheory libTheory semanticPrimitivesTheory - semanticPrimitivesPropsTheory evaluatePropsTheory; + semanticPrimitivesPropsTheory evaluatePropsTheory + fpSemTheory; open mlvectorTheory mlstringTheory packLib; open integer_wordSyntax open terminationTheory @@ -430,6 +431,18 @@ val Eval2_tac = \\ disch_then (qspec_then `ck1'` strip_assume_tac) \\ fs [] \\ qexists_tac `ck1+ck1'` \\ fs []; +val Eval3_tac = + first_x_assum (qspec_then `refs` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ first_x_assum (qspec_then `refs++refs'` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ first_x_assum (qspec_then `refs++refs'++refs''` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ disch_then (qspec_then `ck3` strip_assume_tac) + \\ disch_then (qspec_then `ck2` strip_assume_tac) + \\ disch_then (qspec_then `ck1'` strip_assume_tac) + \\ fs [] \\ qexists_tac `ck1+ck1'+ck1''` \\ fs []; + Theorem Eval_Equality `Eval env x1 (a y1) /\ Eval env x2 (a y2) ==> EqualityType a ==> @@ -1208,6 +1221,82 @@ Theorem Eval_word_ror \\ fs [do_app_def,shift8_lookup_def,shift64_lookup_def] \\ fs [fcpTheory.CART_EQ,word_ror_def,fcpTheory.FCP_BETA,w2w] \\ rw []); +(* arithmetic for doubles (word64) *) + +(* FIXME: FP_top from master *) + (* +val Eval_FP_top = Q.prove ( + `!f w1 w2 w3. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env x2 (WORD (w2:64 word)) ==> + Eval env x3 (WORD (w3:64 word)) ==> + Eval env (App (FP_top f) [x1;x2;x3]) (WORD (fp_top f w1 w2 w3))`, + rw[Eval_rw,WORD_def] + \\ Eval3_tac \\ fs [do_app_def] \\ rw [] + \\ fs [state_component_equality]); + *) + +val Eval_FP_bop = Q.prove( + `!f w1 w2. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env x2 (WORD (w2:64 word)) ==> + Eval env (App (FP_bop f) [x1;x2]) (WORD (fp_bop f w1 w2))`, + rw[Eval_rw,WORD_def] + \\ Eval2_tac \\ fs [do_app_def] \\ rw [] + \\ fs [state_component_equality]); + +local + fun f name q = + save_thm("Eval_" ^ name,SIMP_RULE (srw_ss()) [fp_bop_def] + (Q.SPEC q Eval_FP_bop)) +in + val Eval_FLOAT_ADD = f "FLOAT_ADD" `FP_Add` + val Eval_FLOAT_SUB = f "FLOAT_SUB" `FP_Sub` + val Eval_FLOAT_MULT = f "FLOAT_MULT" `FP_Mul` + val Eval_FLOAT_DIV = f "FLOAT_DIV" `FP_Div` +end; + +val Eval_FP_cmp = Q.prove( + `!f w1 w2. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env x2 (WORD (w2:64 word)) ==> + Eval env (App (FP_cmp f) [x1;x2]) (BOOL (fp_cmp f w1 w2))`, + rw[Eval_rw,WORD_def,BOOL_def] + \\ Eval2_tac \\ fs [do_app_def] \\ rw [] + \\ fs [state_component_equality]); + +local + fun f name q = let + val th = SIMP_RULE (srw_ss()) [fp_cmp_def] (Q.SPEC q Eval_FP_cmp) + val _ = save_thm("Eval_" ^ name,SPEC_ALL th) + in th end +in + val Eval_FLOAT_LESS = f "FLOAT_LESS" `FP_Less` + val Eval_FLOAT_LESS_EQ = f "FLOAT_LESS_EQ" `FP_LessEqual` + val Eval_FLOAT_GREATER = f "FLOAT_GREATER" `FP_Greater` + val Eval_FLOAT_GREATER_EQ = f "FLOAT_GREATER_EQ" `FP_GreaterEqual` + val Eval_FLOAT_EQ = f "FLOAT_EQ" `FP_Equal` +end; + +val Eval_FP_uop = Q.prove( + `!f w1 w2. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env (App (FP_uop f) [x1]) (WORD (fp_uop f w1))`, + rw[Eval_rw,WORD_def,BOOL_def] + \\ first_x_assum (qspec_then `refs` strip_assume_tac) + \\ qexists_tac `ck1` \\ fs[do_app_def, state_component_equality]); + +local + fun f name q = let + val th = SIMP_RULE (srw_ss()) [fp_uop_def] (Q.SPEC q Eval_FP_uop) + val _ = save_thm("Eval_" ^ name,SPEC_ALL th) + in th end +in + val Eval_FLOAT_ABS = f "FLOAT_ABS" `FP_Abs` + val Eval_FLOAT_NEG = f "FLOAT_NEG" `FP_Neg` + val Eval_FLOAT_SQRT = f "FLOAT_SQRT" `FP_Sqrt` +end; + (* list definition *) val LIST_TYPE_def = Define ` diff --git a/translator/ml_translator_testScript.sml b/translator/ml_translator_testScript.sml index 86c31a4ac8..28c21b3ce8 100644 --- a/translator/ml_translator_testScript.sml +++ b/translator/ml_translator_testScript.sml @@ -150,6 +150,12 @@ val test_def = Define`test ids = D (F ids.f) (V ids.v)`; val res = translate test_def; +(* Test floating-point support *) + +val test_def = Define `test f = fp64_add roundTiesToEven f f` + +val res = translate test_def; + (* tricky datatype *) val _ = register_type ``:'a option``; From 918a5d7bcf98329e05c4ee59da2e6d97f0163c4e Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Sun, 12 May 2019 18:41:18 +0200 Subject: [PATCH 2/4] Add support for 64-bit floating-point translation for binary and unary ops --- translator/ml_translatorLib.sml | 18 ++++- translator/ml_translatorScript.sml | 91 ++++++++++++++++++++++++- translator/ml_translator_testScript.sml | 6 ++ 3 files changed, 111 insertions(+), 4 deletions(-) diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index d4c09f05cb..201bf635e1 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -424,9 +424,9 @@ val basic_theories = ["alist", "arithmetic", "bag", "bitstring", "bit", "bool", "combin", "container", "divides", "fcp", "finite_map", "float", "fmaptree", "frac", "gcdset", "gcd", "ind_type", "integer_word", - "integer", "integral", "list", "llist", "marker", "measure", - "numeral_bit", "numeral", "numpair", "numposrep", "num", "one", - "operator", "option", "pair", "path", "patricia_casts", + "integer", "integral", "list", "llist", "marker", "machine_iee", + "measure", "numeral_bit", "numeral", "numpair", "numposrep", "num", + "one", "operator", "option", "pair", "path", "patricia_casts", "patricia", "poly", "poset", "powser", "pred_set", "prelim", "prim_rec", "quote", "quotient_list", "quotient_option", "quotient_pair", "quotient_pred_set", "quotient_sum", "quotient", @@ -2712,6 +2712,15 @@ val builtin_binops = Eval_INT_LESS_EQ, Eval_INT_GREATER, Eval_INT_GREATER_EQ, + Eval_FLOAT_ADD, + Eval_FLOAT_SUB, + Eval_FLOAT_MULT, + Eval_FLOAT_DIV, + Eval_FLOAT_LESS, + Eval_FLOAT_LESS_EQ, + Eval_FLOAT_GREATER, + Eval_FLOAT_GREATER_EQ, + Eval_FLOAT_EQ, Eval_force_gc_to_run, Eval_force_unit_type, Eval_strsub, @@ -2732,6 +2741,9 @@ val builtin_monops = Eval_vector, Eval_int_of_num, Eval_num_of_int, + Eval_FLOAT_ABS, + Eval_FLOAT_SQRT, + Eval_FLOAT_NEG, Eval_empty_ffi, Eval_force_out_of_memory_error, Eval_Chr, diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml index 3e0b66bdd7..39100f5645 100644 --- a/translator/ml_translatorScript.sml +++ b/translator/ml_translatorScript.sml @@ -5,7 +5,8 @@ *) open integerTheory ml_progTheory astTheory libTheory semanticPrimitivesTheory - semanticPrimitivesPropsTheory evaluatePropsTheory; + semanticPrimitivesPropsTheory evaluatePropsTheory + fpSemTheory; open mlvectorTheory mlstringTheory packLib; open integer_wordSyntax open terminationTheory @@ -488,6 +489,18 @@ val Eval2_tac = \\ disch_then (qspec_then `ck1'` strip_assume_tac) \\ fs [] \\ qexists_tac `ck1+ck1'` \\ fs []; +val Eval3_tac = + first_x_assum (qspec_then `refs` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ first_x_assum (qspec_then `refs++refs'` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ first_x_assum (qspec_then `refs++refs'++refs''` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ disch_then (qspec_then `ck3` strip_assume_tac) + \\ disch_then (qspec_then `ck2` strip_assume_tac) + \\ disch_then (qspec_then `ck1'` strip_assume_tac) + \\ fs [] \\ qexists_tac `ck1+ck1'+ck1''` \\ fs []; + Theorem Eval_Equality: Eval env x1 (a y1) /\ Eval env x2 (a y2) ==> EqualityType a ==> @@ -1346,6 +1359,82 @@ Proof \\ fs [fcpTheory.CART_EQ,word_ror_def,fcpTheory.FCP_BETA,w2w] \\ rw [] QED +(* arithmetic for doubles (word64) *) + +(* FIXME: FP_top from master *) + (* +val Eval_FP_top = Q.prove ( + `!f w1 w2 w3. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env x2 (WORD (w2:64 word)) ==> + Eval env x3 (WORD (w3:64 word)) ==> + Eval env (App (FP_top f) [x1;x2;x3]) (WORD (fp_top f w1 w2 w3))`, + rw[Eval_rw,WORD_def] + \\ Eval3_tac \\ fs [do_app_def] \\ rw [] + \\ fs [state_component_equality]); + *) + +val Eval_FP_bop = Q.prove( + `!f w1 w2. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env x2 (WORD (w2:64 word)) ==> + Eval env (App (FP_bop f) [x1;x2]) (WORD (fp_bop f w1 w2))`, + rw[Eval_rw,WORD_def] + \\ Eval2_tac \\ fs [do_app_def] \\ rw [] + \\ fs [state_component_equality]); + +local + fun f name q = + save_thm("Eval_" ^ name,SIMP_RULE (srw_ss()) [fp_bop_def] + (Q.SPEC q Eval_FP_bop)) +in + val Eval_FLOAT_ADD = f "FLOAT_ADD" `FP_Add` + val Eval_FLOAT_SUB = f "FLOAT_SUB" `FP_Sub` + val Eval_FLOAT_MULT = f "FLOAT_MULT" `FP_Mul` + val Eval_FLOAT_DIV = f "FLOAT_DIV" `FP_Div` +end; + +val Eval_FP_cmp = Q.prove( + `!f w1 w2. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env x2 (WORD (w2:64 word)) ==> + Eval env (App (FP_cmp f) [x1;x2]) (BOOL (fp_cmp f w1 w2))`, + rw[Eval_rw,WORD_def,BOOL_def] + \\ Eval2_tac \\ fs [do_app_def] \\ rw [] + \\ fs [state_component_equality]); + +local + fun f name q = let + val th = SIMP_RULE (srw_ss()) [fp_cmp_def] (Q.SPEC q Eval_FP_cmp) + val _ = save_thm("Eval_" ^ name,SPEC_ALL th) + in th end +in + val Eval_FLOAT_LESS = f "FLOAT_LESS" `FP_Less` + val Eval_FLOAT_LESS_EQ = f "FLOAT_LESS_EQ" `FP_LessEqual` + val Eval_FLOAT_GREATER = f "FLOAT_GREATER" `FP_Greater` + val Eval_FLOAT_GREATER_EQ = f "FLOAT_GREATER_EQ" `FP_GreaterEqual` + val Eval_FLOAT_EQ = f "FLOAT_EQ" `FP_Equal` +end; + +val Eval_FP_uop = Q.prove( + `!f w1 w2. + Eval env x1 (WORD (w1:64 word)) ==> + Eval env (App (FP_uop f) [x1]) (WORD (fp_uop f w1))`, + rw[Eval_rw,WORD_def,BOOL_def] + \\ first_x_assum (qspec_then `refs` strip_assume_tac) + \\ qexists_tac `ck1` \\ fs[do_app_def, state_component_equality]); + +local + fun f name q = let + val th = SIMP_RULE (srw_ss()) [fp_uop_def] (Q.SPEC q Eval_FP_uop) + val _ = save_thm("Eval_" ^ name,SPEC_ALL th) + in th end +in + val Eval_FLOAT_ABS = f "FLOAT_ABS" `FP_Abs` + val Eval_FLOAT_NEG = f "FLOAT_NEG" `FP_Neg` + val Eval_FLOAT_SQRT = f "FLOAT_SQRT" `FP_Sqrt` +end; + (* list definition *) val LIST_TYPE_def = Define ` diff --git a/translator/ml_translator_testScript.sml b/translator/ml_translator_testScript.sml index 52a2357ca1..492e1e5dd8 100644 --- a/translator/ml_translator_testScript.sml +++ b/translator/ml_translator_testScript.sml @@ -150,6 +150,12 @@ val test_def = Define`test ids = D (F ids.f) (V ids.v)`; val res = translate test_def; +(* Test floating-point support *) + +val test_def = Define `test f = fp64_add roundTiesToEven f f` + +val res = translate test_def; + (* tricky datatype *) val _ = register_type ``:'a option``; From f87b41a181cd2d1da7b16f74b048e69a616a176d Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Mon, 27 May 2019 14:01:07 +0200 Subject: [PATCH 3/4] Add support for FMA instructions to translator --- translator/ml_translatorLib.sml | 3 +- translator/ml_translatorScript.sml | 49 ++++++++++++++----------- translator/ml_translator_testScript.sml | 6 +++ 3 files changed, 35 insertions(+), 23 deletions(-) diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index 201bf635e1..1725acbdd4 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -2683,7 +2683,8 @@ fun mutual_to_single_line_def def = let in ([def],ind) end val builtin_terops = - [Eval_substring] + [Eval_substring, + Eval_FLOAT_FMA] |> map SPEC_ALL |> map (fn th => (th |> UNDISCH_ALL |> concl |> rand |> rand |> rator |> rator |> rator, th)) diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml index cf3cfb10ef..7c5067093a 100644 --- a/translator/ml_translatorScript.sml +++ b/translator/ml_translatorScript.sml @@ -489,18 +489,6 @@ val Eval2_tac = \\ disch_then (qspec_then `ck1'` strip_assume_tac) \\ fs [] \\ qexists_tac `ck1+ck1'` \\ fs []; -val Eval3_tac = - first_x_assum (qspec_then `refs` strip_assume_tac) - \\ drule evaluate_add_to_clock - \\ first_x_assum (qspec_then `refs++refs'` strip_assume_tac) - \\ drule evaluate_add_to_clock - \\ first_x_assum (qspec_then `refs++refs'++refs''` strip_assume_tac) - \\ drule evaluate_add_to_clock - \\ disch_then (qspec_then `ck3` strip_assume_tac) - \\ disch_then (qspec_then `ck2` strip_assume_tac) - \\ disch_then (qspec_then `ck1'` strip_assume_tac) - \\ fs [] \\ qexists_tac `ck1+ck1'+ck1''` \\ fs []; - Theorem Eval_Equality: Eval env x1 (a y1) /\ Eval env x2 (a y2) ==> EqualityType a ==> @@ -1360,19 +1348,36 @@ Proof QED (* arithmetic for doubles (word64) *) - -(* FIXME: FP_top from master *) - (* -val Eval_FP_top = Q.prove ( - `!f w1 w2 w3. - Eval env x1 (WORD (w1:64 word)) ==> +Theorem Eval_FP_top: + ! f w1 w2 w3. Eval env x2 (WORD (w2:64 word)) ==> Eval env x3 (WORD (w3:64 word)) ==> - Eval env (App (FP_top f) [x1;x2;x3]) (WORD (fp_top f w1 w2 w3))`, + Eval env x1 (WORD (w1:64 word)) ==> + Eval env (App (FP_top f) [x1;x2;x3]) (WORD (fp_top f w1 w2 w3)) +Proof rw[Eval_rw,WORD_def] - \\ Eval3_tac \\ fs [do_app_def] \\ rw [] - \\ fs [state_component_equality]); - *) + \\ first_x_assum mp_tac + \\ first_x_assum (qspec_then `refs` strip_assume_tac) + \\ strip_tac + \\ drule evaluate_add_to_clock + \\ last_x_assum (qspec_then `refs++refs'` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ first_x_assum (qspec_then `refs++refs'++refs''` strip_assume_tac) + \\ drule evaluate_add_to_clock + \\ rpt (disch_then assume_tac) + \\ pop_assum (qspec_then `ck1' + ck1''` strip_assume_tac) + \\ fs[] \\ qexists_tac `ck1 + ck1' + ck1''` \\ fs[] + \\ fs [do_app_def] \\ rw [] + \\ fs [state_component_equality] +QED + +local + fun f name q = + save_thm("Eval_" ^ name,SIMP_RULE (srw_ss()) [fp_top_def, fpfma_def] + (Q.SPEC q Eval_FP_top)) +in + val Eval_FLOAT_FMA = f "FLOAT_FMA" `FP_Fma` +end; val Eval_FP_bop = Q.prove( `!f w1 w2. diff --git a/translator/ml_translator_testScript.sml b/translator/ml_translator_testScript.sml index 492e1e5dd8..a1a51a9b21 100644 --- a/translator/ml_translator_testScript.sml +++ b/translator/ml_translator_testScript.sml @@ -156,6 +156,12 @@ val test_def = Define `test f = fp64_add roundTiesToEven f f` val res = translate test_def; +(* FMA: *) + +val test_def = Define `test f1 f2 f3 = (fp64_mul_add roundTiesToEven) f1 f2 f3` + +val res = translate test_def; + (* tricky datatype *) val _ = register_type ``:'a option``; From cdbaff76d00446aa615a4afa7af1098d32c70221 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Wed, 29 May 2019 13:48:50 +0200 Subject: [PATCH 4/4] Fix typo in translator/ml_translatorlib.sml --- translator/ml_translatorLib.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml index 1725acbdd4..63057409c9 100644 --- a/translator/ml_translatorLib.sml +++ b/translator/ml_translatorLib.sml @@ -424,7 +424,7 @@ val basic_theories = ["alist", "arithmetic", "bag", "bitstring", "bit", "bool", "combin", "container", "divides", "fcp", "finite_map", "float", "fmaptree", "frac", "gcdset", "gcd", "ind_type", "integer_word", - "integer", "integral", "list", "llist", "marker", "machine_iee", + "integer", "integral", "list", "llist", "marker", "machine_ieee", "measure", "numeral_bit", "numeral", "numpair", "numposrep", "num", "one", "operator", "option", "pair", "path", "patricia_casts", "patricia", "poly", "poset", "powser", "pred_set", "prelim",