Skip to content

Commit

Permalink
Fixed the CakeML-exported VSS example, some additions to V1Model
Browse files Browse the repository at this point in the history
  • Loading branch information
@didriklundberg
didriklundberg committed Dec 29, 2024
1 parent b10253f commit 5222db7
Show file tree
Hide file tree
Showing 5 changed files with 85 additions and 51 deletions.
60 changes: 36 additions & 24 deletions hol/cake_export/p4_vss_example_cakeProgScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory ml
open p4_exec_sem_vss_cakeProgTheory;

val _ = intLib.deprecate_int();
val _ = (max_print_depth := 100);
val _ = (max_print_depth := 1000);

val _ = translation_extends "p4_exec_sem_vss_cakeProg";

Expand Down Expand Up @@ -332,7 +332,7 @@ val vss_astate = “((0,
("action_run",v_bit (REPLICATE 32 F,32))],NONE)]],
arch_frame_list_empty,status_running):vss_ascope astate”;

val n_max = “180:num”;
val n_max = “205:num”;

(*
Expand All @@ -345,32 +345,44 @@ fun deparse_bool_list l =
else (#"0"::(deparse_bool_list t))
;
(* From VSS TTL example, with symbolic bits made concrete with arbitrary values *)
val input = “([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; T; F; F; F; F; F; F; F; F; F;
F; F; F; T; F; F; F; T; F; T; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; T; F; T; F; F;
F; F; F; F; F; F; F; T; F; T; F; F; F;
F; F; F; F; F; F; F; T; F; T; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; T; F; F;
F; F; F; F; F; F; F; T; F; T; F; F; F;
F; F; F; F; F; F; F; T; F; T; F;
F; F; F; F; F; F; F; T; F; T;
F; F; F; F; F; F; F; T; F;
F; F; F; F; F; F; F; T; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F],1:num)”;
(* Code from VSS example, generating input *)
val input_port_ok = ``1:num``;
val input_data_ok = listSyntax.mk_list ([], bool);
val input_ttl_ok = 1;
val input_ipv4_ok = p4_testLib.mk_ipv4_packet_ok input_data_ok input_ttl_ok;
val input_ok = p4_testLib.mk_eth_frame_ok input_ipv4_ok;
(* From VSS TTL example, with symbolic bits made concrete with zeroed values *)
val input = “([F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; T; F; F; F; F; F; F; F; F; F; F; F; F; T; F; F; F; T; F; T;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; T; F; T; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; T; F; F; F; F; F; F; F; F;
T; F; T; T; T; F; F; T; T; T; T; F; T; F; T; T; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F;
F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F],1:num)”;
val bl_input_tm = fst $ dest_pair input
(* Entire state after a number of steps *)
EVAL “arch_multi_exec ^vss_actx (p4_append_input_list [^input] ^vss_astate) 120”
EVAL “vss_exec ^input”
EVAL “arch_multi_exec ^vss_actx (p4_append_input_list [^input] ^vss_astate) 181”
val cake_top_exec_def =
Define
‘cake_top_exec input =
case
arch_multi_exec' ^vss_actx
(p4_append_input_list [input] ^vss_astate) ^n_max of
| SOME res => SOME $ p4_get_output_list res
| NONE => NONE’;
EVAL “cake_top_exec ^input”
EVAL “arch_multi_exec' ^vss_actx (p4_append_input_list [^input] ^vss_astate) ^n_max”
val bl_input = String.implode $ deparse_bool_list $ fst $ listSyntax.dest_list bl_input_tm
Expand Down
2 changes: 1 addition & 1 deletion hol/cake_export/vss_test.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,5 @@ cp ${progname}.sexp test/
cd test
./compile_test_cake.sh ${progname}
# TODO: This packet is expected to be dropped. Hard-code some tables to obtain a better example.
time ./${progname}.cake 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000010001010000000000000000000101000000000101000000000010100000000000000001000000000101000000000010100000000101000000010000000010000000000000000000000000000000000000000000000000000000000000000000 1
time ./${progname}.cake 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000100000000000010001010000000000000000000101000000000000000000000000000000000000000001000000001011100111101011000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 1
cd ..
40 changes: 19 additions & 21 deletions hol/p4_testLib.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -482,7 +482,9 @@ fun replace_ext_impl ctx_tm ext_name method_name method_tm =

val ext_map' =
let
val res_opt = rhs $ concl $ EVAL ``ext_map_replace_impl ^ext_map ^(stringLib.fromMLstring ext_name) ^(stringLib.fromMLstring method_name) ^method_tm``;
val ext_name_tm = stringLib.fromMLstring ext_name
val method_name_tm = stringLib.fromMLstring method_name
val res_opt = rhs $ concl $ EVAL ``ext_map_replace_impl ^ext_map ^ext_name_tm ^method_name_tm ^method_tm``;
in
if is_some res_opt
then dest_some res_opt
Expand All @@ -497,28 +499,24 @@ fun replace_ext_impl ctx_tm ext_name method_name method_tm =
end
;

fun replace_ext_impl ctx_tm ext_name method_name method_tm =
fun update_table astate table_name new_entry =
let
val actx_list = spine_pair ctx_tm;

val actx_list_8first = List.take (actx_list, 8);

val ext_map = el 9 actx_list;

val ext_map' =
let
val res_opt = rhs $ concl $ EVAL ``ext_map_replace_impl ^ext_map ^(stringLib.fromMLstring ext_name) ^(stringLib.fromMLstring method_name) ^method_tm``;
in
if is_some res_opt
then dest_some res_opt
else raise (mk_HOL_ERR "p4_testLib" "replace_ext_impl" ("extern name "^ext_name^" and/or method name "^method_name^" could not be found in ext_map"))
end;

val actx_list_10 = List.last actx_list;
val actx_list' = (actx_list_8first@[ext_map'])@[actx_list_10];
val actx' = list_mk_pair actx_list';
val (aenv, g_scope_list, arch_frame_list, status) = dest_astate astate
(* TODO: Danger: not generic *)
val (i, in_out_list, in_out_list', scope) = dest_aenv aenv
val (counter, ext_obj_map, v_map, ctrl) = dest_ascope scope
(* TODO: Handle error *)
val table_config = dest_some $ rhs $ concl $ EVAL “ALOOKUP ^ctrl ^table_name”
(* Simply put the new entry in the front *)
val table_config' = rhs $ concl $ EVAL “CONS ^new_entry ^table_config”
(* Update the table *)
val ctrl' = dest_some $ rhs $ concl $ EVAL “AUPDATE ^ctrl (^table_name, ^table_config')”

val ascope' = list_mk_pair [counter, ext_obj_map, v_map, ctrl']
val aenv' = mk_aenv (i, in_out_list, in_out_list', ascope')
val astate' = mk_astate (aenv', g_scope_list, arch_frame_list, status)
in
actx'
astate'
end
;

Expand Down
4 changes: 3 additions & 1 deletion hol/p4_v1modelLib.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,9 @@ val v1model_objectless_map =
``[("mark_to_drop", ([("standard_metadata", d_inout)], v1model_mark_to_drop));
("verify", ([("condition", d_in); ("err", d_in)], v1model_verify));
("verify_checksum", ([("condition", d_in); ("data", d_in); ("checksum", d_in); ("algo", d_none)], v1model_verify_checksum));
("update_checksum", ([("condition", d_in); ("data", d_in); ("checksum", d_inout); ("algo", d_none)], v1model_update_checksum))]``;
("update_checksum", ([("condition", d_in); ("data", d_in); ("checksum", d_inout); ("algo", d_none)], v1model_update_checksum));
("assert", ([("check", d_in)], v1model_assert));
("assume", ([("check", d_in)], v1model_assume))]``;

val v1model_packet_in_map =
``[("extract", ([("this", d_in); ("headerLvalue", d_out)], v1model_packet_in_extract));
Expand Down
30 changes: 26 additions & 4 deletions hol/p4_v1modelScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ Datatype:
(* From IPSec example *)
| v1model_v_ext_ipsec_crypt
End
val _ = type_abbrev("v1model_sum_v_ext", ``:(core_v_ext, v1model_v_ext) sum``);
val _ = type_abbrev("v1model_sum_v_ext", “:(core_v_ext, v1model_v_ext) sum”);

(* The control plane representation:
Expand All @@ -45,10 +45,10 @@ val _ = type_abbrev("v1model_sum_v_ext", ``:(core_v_ext, v1model_v_ext) sum``);
(* the action of a table entry: string is action name, e_list is arguments *)
string # e_list) alist) alist``)
*)
val _ = type_abbrev("v1model_ctrl", ``:(string, (((e_list -> bool) # num), string # e_list) alist) alist``);
val _ = type_abbrev("v1model_ctrl", “:(string, (((e_list -> bool) # num), string # e_list) alist) alist”);

(* The architectural state type of the V1Model architecture model *)
val _ = type_abbrev("v1model_ascope", ``:(num # ((num, v1model_sum_v_ext) alist) # ((string, v) alist) # v1model_ctrl)``);
val _ = type_abbrev("v1model_ascope", “:(num # ((num, v1model_sum_v_ext) alist) # ((string, v) alist) # v1model_ctrl)”);

(**********************************************************)
(* SPECIALISED CORE METHODS *)
Expand Down Expand Up @@ -124,6 +124,28 @@ Definition v1model_mark_to_drop_def:
| NONE => NONE
End

(* TODO: Need new functionality to exit pipeline immediately... Currently, this will just return NONE instead *)
Definition v1model_assert_def:
v1model_assert (v1model_ascope:v1model_ascope, g_scope_list:g_scope_list, scope_list) =
case lookup_lval' scope_list (lval_varname (varn_name "check")) of
| SOME $ v_bool b =>
(if b
then SOME (v1model_ascope, scope_list, status_returnv v_bot)
else NONE)
| _ => NONE
End

(* Assumptions also cause the program to fail when not holding apparently... *)
Definition v1model_assume_def:
v1model_assume (v1model_ascope:v1model_ascope, g_scope_list:g_scope_list, scope_list) =
case lookup_lval' scope_list (lval_varname (varn_name "check")) of
| SOME $ v_bool b =>
(if b
then SOME (v1model_ascope, scope_list, status_returnv v_bot)
else NONE)
| _ => NONE
End

(**********************)
(* Checksum methods *)
(**********************)
Expand Down Expand Up @@ -234,7 +256,7 @@ Definition v1model_verify_checksum_def:
)
End

(*************************)
(*******************)
(* update_checksum *)

Definition v1model_update_checksum_inner_def:
Expand Down

0 comments on commit 5222db7

Please sign in to comment.