From b2d438ad2f1a671163687f9b44832c5f39980b0f Mon Sep 17 00:00:00 2001 From: Didrik Lundberg Date: Fri, 20 Dec 2024 17:26:04 +0100 Subject: [PATCH] Function library for CakeML export of HOL4P4 programs --- hol/cake_export/p4_cake_wrapperLib.sig | 7 + hol/cake_export/p4_cake_wrapperLib.sml | 120 ++++++++++++++++++ .../p4_conditional_cakeProgScript.sml | 9 +- .../p4_exec_sem_arch_cakeProgScript.sml | 7 + .../p4_exec_sem_v1model_cakeProgScript.sml | 5 - .../p4_exec_sem_vss_cakeProgScript.sml | 5 - .../p4_vss_example_cakeProgScript.sml | 14 +- 7 files changed, 149 insertions(+), 18 deletions(-) create mode 100644 hol/cake_export/p4_cake_wrapperLib.sig create mode 100644 hol/cake_export/p4_cake_wrapperLib.sml diff --git a/hol/cake_export/p4_cake_wrapperLib.sig b/hol/cake_export/p4_cake_wrapperLib.sig new file mode 100644 index 0000000..d7256a2 --- /dev/null +++ b/hol/cake_export/p4_cake_wrapperLib.sig @@ -0,0 +1,7 @@ +signature p4_cake_wrapperLib = +sig + include Abbrev + +val translate_p4 : string -> term -> term -> term -> unit + +end diff --git a/hol/cake_export/p4_cake_wrapperLib.sml b/hol/cake_export/p4_cake_wrapperLib.sml new file mode 100644 index 0000000..d36327d --- /dev/null +++ b/hol/cake_export/p4_cake_wrapperLib.sml @@ -0,0 +1,120 @@ +structure p4_cake_wrapperLib :> p4_cake_wrapperLib = struct + +open HolKernel boolLib Parse bossLib; + +open p4Syntax; +open bitstringSyntax numSyntax; +open p4Theory; +open p4_auxTheory; +open p4_exec_semTheory; +open p4_coreTheory p4_vssTheory; + +(* CakeML: *) +open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory mlmapTheory basisFunctionsLib + astPP comparisonTheory; +open fromSexpTheory; + +val _ = intLib.deprecate_int(); + +(* Note that this function only adds inlined CakeML code - it translates no HOL4 + * definitions. + * The function provides a command-line interface that passes an incoming packet in a + * format of ones and zeroes (e.g. "1010010001010101") and an ingress port in the format + * of a number (e.g. "42"). This is then used as input to the top-level execution function + * cake_top_exec. *) +fun append_prog_p4_wrapper () = + let + val _ = append_prog o process_topdecs $ + ‘exception ParseError string;’ + ; + + val _ = append_prog o process_topdecs $ + ‘fun parse_bool_list l = + case l of + [] => [] + | h::t => + if h = #"0" + then (False::(parse_bool_list t)) + else if h = #"1" + then (True::(parse_bool_list t)) + else raise ParseError ("Error: packet (first command-line argument) should be specified using only 0s and 1s to signify bits.\n") + ; + ’; + + val _ = append_prog o process_topdecs $ + ‘fun deparse_bool_list l = + case l of + [] => [] + | h::t => + if h + then (#"T"::(deparse_bool_list t)) + else (#"F"::(deparse_bool_list t)) + ;’; + + val _ = append_prog o process_topdecs $ + ‘fun print_output_packets l = + case l of + [] => () + | (out_bl, out_port)::t => + let + val out_packet_string = String.implode (deparse_bool_list out_bl) + in + print(out_packet_string ^ " at port "); print_int out_port; print "\n"; print_output_packets t + end + ;’; + + val _ = append_prog o process_topdecs $ + ‘fun main () = + let + val packet_arg::rest = (CommandLine.arguments()) + val port_arg = List.hd rest + + val bl = parse_bool_list (String.explode packet_arg) + val in_port = Option.valOf (Int.fromString port_arg) + val in_packet_string = String.implode (deparse_bool_list bl) + in + (case cake_top_exec (bl, in_port) of + None => raise ParseError ("Error: execution result is None.\n") + | Some output_packets => + (print ("Input packet was: " ^ in_packet_string ^ " at port "); print_int in_port; print "\n"; + print "Output packet(s) are: "; print_output_packets output_packets)) + end + handle ParseError parse_err_msg => TextIO.print_err parse_err_msg + handle _ => + TextIO.print_err ("Usage: " ^ CommandLine.name() ^ " \n");’; + in + (* TODO: Can this be replaced with something more short-handish? *) + “SNOC + (Dlet unknown_loc (Pcon NONE []) + (App Opapp [Var (Short "main"); Con NONE []])) + ^(get_ml_prog_state() |> get_prog)” + |> EVAL |> concl |> rhs + end +; + +(* This function takes a program name as a string (e.g. "test_program", without suffix), + * an actx and astate (HOL4 terms which can be obtained from the HOL4P4 import tool) + * a maximum number of reduction steps (e.g. 140) and then constructs a CakeML sexp that + * can be compiled to a command-line program that concretely executes the P4 program in + * actx from the initial state astate, then prints the resulting outgoing packets. *) +fun translate_p4 progname actx astate n_max = + let + val cake_top_exec_def = + Define + ‘cake_top_exec input = + case + arch_multi_exec' ^actx + (p4_append_input_list [input] ^astate) ^n_max of + | SOME res => SOME $ p4_get_output_list res + | NONE => NONE’; + + (* TODO: This is the bottleneck... *) + val _ = translate cake_top_exec_def; + + val prog = append_prog_p4_wrapper (); + in + astToSexprLib.write_ast_to_file (progname^".sexp") prog + end +; + +end diff --git a/hol/cake_export/p4_conditional_cakeProgScript.sml b/hol/cake_export/p4_conditional_cakeProgScript.sml index baf1c20..f9ca108 100644 --- a/hol/cake_export/p4_conditional_cakeProgScript.sml +++ b/hol/cake_export/p4_conditional_cakeProgScript.sml @@ -14,9 +14,9 @@ open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory ml astPP comparisonTheory; open p4_exec_sem_v1model_cakeProgTheory; - +(* open fromSexpTheory; - +*) intLib.deprecate_int(); val _ = (max_print_depth := 1000); @@ -146,7 +146,7 @@ val symb_exec1_astate = “((0,[],[],0,[],[("parseError",v_bit (fixwidth 32 (n2v (* 44 seems to work also with arch_multi_exec, 45 doesn't work *) val n_max = “45:num”; - +(* (*************************) (* Generic wrapper parts *) @@ -283,5 +283,8 @@ val prog = |> EVAL |> concl |> rhs; val _ = astToSexprLib.write_ast_to_file "conditional_test.sexp" prog; +*) + +p4_cake_wrapperLib.translate_p4 "conditional_example" symb_exec1_actx symb_exec1_astate n_max; val _ = export_theory (); diff --git a/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml index cadbbc4..12fbb80 100644 --- a/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml +++ b/hol/cake_export/p4_exec_sem_arch_cakeProgScript.sml @@ -138,6 +138,10 @@ Definition arch_multi_exec'_def: | NONE => NONE) End +Definition p4_get_output_list_def: + p4_get_output_list (((i, io_list, io_list', ascope), g_scope_list, arch_frame_list, status):'a astate) = + io_list' +End val _ = translation_extends "p4_exec_sem_frames_cakeProg"; @@ -157,6 +161,9 @@ val _ = translate arch_exec'_def; val _ = translate arch_multi_exec'_def; +val _ = translate p4_append_input_list_def; +val _ = translate p4_get_output_list_def; + val _ = ml_prog_update (close_module NONE); val _ = export_theory (); diff --git a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml index 84c76a7..418b921 100644 --- a/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml +++ b/hol/cake_export/p4_exec_sem_v1model_cakeProgScript.sml @@ -213,11 +213,6 @@ Definition arch_multi_exec'_def: | NONE => SOME (aenv, g_scope_list, arch_frame_list, status)) End -Definition p4_get_output_list_def: - p4_get_output_list (((i, io_list, io_list', ascope), g_scope_list, arch_frame_list, status):'a astate) = - io_list' -End - val _ = translation_extends "p4_exec_sem_arch_cakeProg"; diff --git a/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml b/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml index 0840f92..d8d20de 100644 --- a/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml +++ b/hol/cake_export/p4_exec_sem_vss_cakeProgScript.sml @@ -201,11 +201,6 @@ Definition arch_multi_exec'_def: | NONE => SOME (aenv, g_scope_list, arch_frame_list, status)) End -Definition p4_get_output_list_def: - p4_get_output_list (((i, io_list, io_list', ascope), g_scope_list, arch_frame_list, status):'a astate) = - io_list' -End - fun mk_v_bitii' (num, width) = let val width_tm = numSyntax.term_of_int width diff --git a/hol/cake_export/p4_vss_example_cakeProgScript.sml b/hol/cake_export/p4_vss_example_cakeProgScript.sml index 3becfde..f5e86af 100644 --- a/hol/cake_export/p4_vss_example_cakeProgScript.sml +++ b/hol/cake_export/p4_vss_example_cakeProgScript.sml @@ -14,10 +14,10 @@ open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory ml astPP comparisonTheory; open p4_exec_sem_vss_cakeProgTheory; - +(* open fromSexpTheory; - -intLib.deprecate_int(); +*) +val _ = intLib.deprecate_int(); val _ = (max_print_depth := 100); val _ = translation_extends "p4_exec_sem_vss_cakeProg"; @@ -336,7 +336,7 @@ val vss_astate = “((0, val n_max = “180:num”; - +(* (*************************) (* Generic wrapper parts *) @@ -488,5 +488,9 @@ val prog = |> EVAL |> concl |> rhs; val _ = astToSexprLib.write_ast_to_file "vss_example.sexp" prog; - +*) + +p4_cake_wrapperLib.translate_p4 "vss_example" vss_actx vss_astate n_max; + + val _ = export_theory ();