From 426f368cc7950a8bc360888befdf75c9f0def972 Mon Sep 17 00:00:00 2001 From: Ali Kheradmand Date: Wed, 4 Apr 2018 01:57:27 -0400 Subject: [PATCH] 13 goes through although it is non-deterministic: only goes through when using debug mode (https://github.com/kframework/k-legacy/issues/2408) --- .../simple/13imppp-5syncpoints-spec.k | 151 ++++ .../simple/13p4-5syncpoints-spec.k | 742 ++++++++++++++++++ tranlation-validation/simple/kkompile.sh | 4 + tranlation-validation/simple/psrun13.sh | 1 + 4 files changed, 898 insertions(+) create mode 100644 tranlation-validation/simple/13imppp-5syncpoints-spec.k create mode 100644 tranlation-validation/simple/13p4-5syncpoints-spec.k create mode 100755 tranlation-validation/simple/kkompile.sh create mode 100755 tranlation-validation/simple/psrun13.sh diff --git a/tranlation-validation/simple/13imppp-5syncpoints-spec.k b/tranlation-validation/simple/13imppp-5syncpoints-spec.k new file mode 100644 index 0000000..ede3a1d --- /dev/null +++ b/tranlation-validation/simple/13imppp-5syncpoints-spec.k @@ -0,0 +1,151 @@ + +module IMPPP-SPEC + imports IMPPP + +syntax Id ::= "h_t" [token] | "h1_f1" [token] | "h1_f2" [token] | "h1_valid" [token] + | "ingress" [token] | "t" [token] | "a" [token] | "b" [token] | "start" [token] + | "parse" [token] | "apply_t" [token] | "process_packet" [token] | "deparse" [token] | "index" [token] | "n" [token] + +rule + + main ( .Exps ) ; + h1_f1 |-> 0 h1_f2 |-> 0 h1_valid |-> false standard_metadata_egress_spec |-> 0 + + start |-> $fun ( .Params , { if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f1 = #extract_next ( 8 , ( false , .Exps ) ) ; if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f2 = #extract_next ( 8 , ( false , .Exps ) ) ; h1_valid = true ; return true ; } ) + apply_t |-> $fun ( .Params , { while ( #get_next_enrty ( .Exps ) ) { if ( #entry_matches ( h1_f1 , .Exps ) ) { #call_entry_action ( .Exps ) ; return 0 ; } } if ( #has_default_action ( .Exps ) ) { #call_default_action ( .Exps ) ; } } ) + parse |-> $fun ( .Params , { return start ( .Exps ) ; } ) + b |-> $fun ( .Params , { standard_metadata_egress_spec = 2 ; } ) + process_packet |-> $fun ( .Params , { #reset ( .Exps ) ; standard_metadata_egress_spec = -1 ; h1_valid = false ; if ( ! ( parse ( .Exps ) ) ) { return false ; } apply_t ( .Exps ) ; if ( standard_metadata_egress_spec == -1 ) { return false ; } return true ; } ) + a |-> $fun ( ( int n ) , .Params , { h1_f2 = n ; standard_metadata_egress_spec = 1 ; } ) + deparse |-> $fun ( .Params , { #emit ( h1_f1 , ( 8 , ( false , .Exps ) ) ) ; ( #emit ( h1_f2 , ( 8 , ( false , .Exps ) ) ) ) ; ( #add_payload ( .Exps ) ) ; } ) + main |-> $fun ( .Params , { while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } } ) + + .List + I:PacketList + $nilPacketList + @nil + @nil + T:EntryList
+ $nilEntryList + _ + 0 + D:DefaultEntry + +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #noUndefPacketList(I) +ensures vars(ListItem(I) ListItem(T) ListItem(D)) +//ensures vars(ListItem(T) ListItem(0)) + +rule + + #get_next_packet ( .Exps ) ~> `#freezerif(_)_else_1` ( { { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } } , { } ) ~> return 0 ; + h1_f1 |-> _:Int h1_f2 |-> _:Int h1_valid |-> _:Bool standard_metadata_egress_spec |-> _:Int + + start |-> $fun ( .Params , { if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f1 = #extract_next ( 8 , ( false , .Exps ) ) ; if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f2 = #extract_next ( 8 , ( false , .Exps ) ) ; h1_valid = true ; return true ; } ) + apply_t |-> $fun ( .Params , { while ( #get_next_enrty ( .Exps ) ) { if ( #entry_matches ( h1_f1 , .Exps ) ) { #call_entry_action ( .Exps ) ; return 0 ; } } if ( #has_default_action ( .Exps ) ) { #call_default_action ( .Exps ) ; } } ) + parse |-> $fun ( .Params , { return start ( .Exps ) ; } ) + b |-> $fun ( .Params , { standard_metadata_egress_spec = 2 ; } ) + process_packet |-> $fun ( .Params , { #reset ( .Exps ) ; standard_metadata_egress_spec = -1 ; h1_valid = false ; if ( ! ( parse ( .Exps ) ) ) { return false ; } apply_t ( .Exps ) ; if ( standard_metadata_egress_spec == -1 ) { return false ; } return true ; } ) + a |-> $fun ( ( int n ) , .Params , { h1_f2 = n ; standard_metadata_egress_spec = 1 ; } ) + deparse |-> $fun ( .Params , { #emit ( h1_f1 , ( 8 , ( false , .Exps ) ) ) ; ( #emit ( h1_f2 , ( 8 , ( false , .Exps ) ) ) ) ; ( #add_payload ( .Exps ) ) ; } ) + main |-> $fun ( .Params , { while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } } ) + + ListItem ( $cnt ( .Params , `#freezer_;0` ( .KList ) ) ) + I:PacketList + O:PacketList + _ + _ + T:EntryList
+ _ + _ + _ + D:DefaultEntry + +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #noUndefPacketList(I) +ensures vars(ListItem(T) ListItem(I) ListItem(O) ListItem(D)) + +rule + + #get_next_enrty ( .Exps ) ~> `#freezerif(_)_else_1` ( { { if ( #entry_matches ( h1_f1 , .Exps ) ) { #call_entry_action ( .Exps ) ; return 0 ; } } while ( #get_next_enrty ( .Exps ) ) { if ( #entry_matches ( h1_f1 , .Exps ) ) { #call_entry_action ( .Exps ) ; return 0 ; } } } , { } ) ~> ( if ( #has_default_action ( .Exps ) ) { #call_default_action ( .Exps ) ; } ) ~> return 0 ; + h1_f1 |-> F1:Int h1_f2 |-> F2:Int h1_valid |-> true standard_metadata_egress_spec |-> E:Int + + start |-> $fun ( .Params , { if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f1 = #extract_next ( 8 , ( false , .Exps ) ) ; if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f2 = #extract_next ( 8 , ( false , .Exps ) ) ; h1_valid = true ; return true ; } ) + apply_t |-> $fun ( .Params , { while ( #get_next_enrty ( .Exps ) ) { if ( #entry_matches ( h1_f1 , .Exps ) ) { #call_entry_action ( .Exps ) ; return 0 ; } } if ( #has_default_action ( .Exps ) ) { #call_default_action ( .Exps ) ; } } ) + parse |-> $fun ( .Params , { return start ( .Exps ) ; } ) + b |-> $fun ( .Params , { standard_metadata_egress_spec = 2 ; } ) + process_packet |-> $fun ( .Params , { #reset ( .Exps ) ; standard_metadata_egress_spec = -1 ; h1_valid = false ; if ( ! ( parse ( .Exps ) ) ) { return false ; } apply_t ( .Exps ) ; if ( standard_metadata_egress_spec == -1 ) { return false ; } return true ; } ) + a |-> $fun ( ( int n ) , .Params , { h1_f2 = n ; standard_metadata_egress_spec = 1 ; } ) + deparse |-> $fun ( .Params , { #emit ( h1_f1 , ( 8 , ( false , .Exps ) ) ) ; ( #emit ( h1_f2 , ( 8 , ( false , .Exps ) ) ) ) ; ( #add_payload ( .Exps ) ) ; } ) + main |-> $fun ( .Params , { while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } } ) + + ListItem ( $cnt ( .Params , `#freezer_;0` ( .KList ) ~> ( if ( standard_metadata_egress_spec == -1 ) { return false ; } ) ~> return true ; ~> return 0 ; ) ) ListItem ( $cnt ( .Params , `#freezer!_0` ( .KList ) ~> `#freezerif(_)_else_1` ( { #drop ( .Exps ) ; } , { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } ) ~> ( while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } ) ~> return 0 ; ) ) ListItem ( $cnt ( .Params , `#freezer_;0` ( .KList ) ) ) + I:PacketList + O:PacketList + Payload:Vals + @nil + T:EntryList
+ C:EntryList + _ + _ + D:DefaultEntry + +//ensures vars(ListItem(L) ListItem(T)) +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #wellDefTable(C) andBool #noUndefPacketList(I) //andBool #noUndefPacket(Payload) +ensures vars(ListItem(I) ListItem(O) ListItem(T) ListItem(C) ListItem(F1) ListItem(F2) ListItem(E) ListItem(D) ListItem(Payload)) +//*** CE should not be the same + +rule + + @call #add_payload ( @nilIVals ) ~> `#freezer_;0` ( .KList ) ~> return 0 ; + h1_f1 |-> _:Int h1_f2 |-> _:Int h1_valid |-> _:Bool standard_metadata_egress_spec |-> E:Int + + start |-> $fun ( .Params , { if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f1 = #extract_next ( 8 , ( false , .Exps ) ) ; if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f2 = #extract_next ( 8 , ( false , .Exps ) ) ; h1_valid = true ; return true ; } ) + apply_t |-> $fun ( .Params , { while ( #get_next_enrty ( .Exps ) ) { if ( #entry_matches ( h1_f1 , .Exps ) ) { #call_entry_action ( .Exps ) ; return 0 ; } } if ( #has_default_action ( .Exps ) ) { #call_default_action ( .Exps ) ; } } ) + parse |-> $fun ( .Params , { return start ( .Exps ) ; } ) + b |-> $fun ( .Params , { standard_metadata_egress_spec = 2 ; } ) + process_packet |-> $fun ( .Params , { #reset ( .Exps ) ; standard_metadata_egress_spec = -1 ; h1_valid = false ; if ( ! ( parse ( .Exps ) ) ) { return false ; } apply_t ( .Exps ) ; if ( standard_metadata_egress_spec == -1 ) { return false ; } return true ; } ) + a |-> $fun ( ( int n ) , .Params , { h1_f2 = n ; standard_metadata_egress_spec = 1 ; } ) + deparse |-> $fun ( .Params , { #emit ( h1_f1 , ( 8 , ( false , .Exps ) ) ) ; ( #emit ( h1_f2 , ( 8 , ( false , .Exps ) ) ) ) ; ( #add_payload ( .Exps ) ) ; } ) + main |-> $fun ( .Params , { while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } } ) + + ListItem ( $cnt ( .Params , `#freezer_;0` ( .KList ) ~> ( #output_packet ( .Exps ) ; ) ~> ( while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } ) ~> return 0 ; ) ) ListItem ( $cnt ( .Params , `#freezer_;0` ( .KList ) ) ) + I:PacketList + O:PacketList + Payload:Vals + PO:Vals + T:EntryList
+ _ + _ + _ + D:DefaultEntry + +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #noUndefPacketList(I) +ensures vars(ListItem(I) ListItem(O) ListItem(T) ListItem(E) ListItem(PO) ListItem(Payload) ListItem(D)) + +rule + + .K + h1_f1 |-> _ h1_f2 |-> _ h1_valid |-> _ standard_metadata_egress_spec |-> _ + + start |-> $fun ( .Params , { if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f1 = #extract_next ( 8 , ( false , .Exps ) ) ; if ( ! ( #has_next ( 8 , .Exps ) ) ) { return false ; } h1_f2 = #extract_next ( 8 , ( false , .Exps ) ) ; h1_valid = true ; return true ; } ) + apply_t |-> $fun ( .Params , { while ( #get_next_enrty ( .Exps ) ) { if ( #entry_matches ( h1_f1 , .Exps ) ) { #call_entry_action ( .Exps ) ; return 0 ; } } if ( #has_default_action ( .Exps ) ) { #call_default_action ( .Exps ) ; } } ) + parse |-> $fun ( .Params , { return start ( .Exps ) ; } ) + b |-> $fun ( .Params , { standard_metadata_egress_spec = 2 ; } ) + process_packet |-> $fun ( .Params , { #reset ( .Exps ) ; standard_metadata_egress_spec = -1 ; h1_valid = false ; if ( ! ( parse ( .Exps ) ) ) { return false ; } apply_t ( .Exps ) ; if ( standard_metadata_egress_spec == -1 ) { return false ; } return true ; } ) + a |-> $fun ( ( int n ) , .Params , { h1_f2 = n ; standard_metadata_egress_spec = 1 ; } ) + deparse |-> $fun ( .Params , { #emit ( h1_f1 , ( 8 , ( false , .Exps ) ) ) ; ( #emit ( h1_f2 , ( 8 , ( false , .Exps ) ) ) ) ; ( #add_payload ( .Exps ) ) ; } ) + main |-> $fun ( .Params , { while ( #get_next_packet ( .Exps ) ) { if ( ! ( process_packet ( .Exps ) ) ) { #drop ( .Exps ) ; } else { deparse ( .Exps ) ; ( #output_packet ( .Exps ) ) ; } } } ) + + .List + $nilPacketList + O:PacketList + _ + _ + _
+ _ + _ + _ + _ + +ensures vars(ListItem(O) ListItem(0)) +[trusted] +endmodule diff --git a/tranlation-validation/simple/13p4-5syncpoints-spec.k b/tranlation-validation/simple/13p4-5syncpoints-spec.k new file mode 100644 index 0000000..be2865b --- /dev/null +++ b/tranlation-validation/simple/13p4-5syncpoints-spec.k @@ -0,0 +1,742 @@ + +module P4-SPEC + imports P4-SEMANTICS + +syntax Id ::= "h_t" [token] | "h1" [token] | "f1" [token] | "n" [token] | "f2" [token]| "ingress" [token] | "t" [token] | "a" [token] | "b" [token] + +//rule +// +// @exec +// +//
+// %standard_metadata_t +// .Map +// ingress_port : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( egress_spec : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +//
+//
+// h_t +// "$fixed_width" |-> 16 +// f1 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( f2 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +//
+// +// .Map +// .Bag +// .Bag +// .Bag +// +// +// true +// true +// %standard_metadata_t +// standard_metadata +// ingress_port |-> _:Val egress_spec |-> _:Val +// +// +// false +// false +// h_t +// h1 +// .Map +// +// +// INITINSTANCES +// .Map +// +// +// start +// ( extract ( h1 ) ; .ExtractOrSetStatements ) return ingress ; +// +// +// .Bag +// .Bag +// .Set +// .Bag +// .Map +// +// +// b +// .ParamList +// modify_field ( ( standard_metadata . egress_spec ) , ( #token("2","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements +// +// +// a +// n , .ParamList +// modify_field ( ( h1 . f2 ) , ( n , .Args ) ) ; ( modify_field ( ( standard_metadata . egress_spec ) , ( #token("1","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements ) +// +// +// .Bag +// .Bag +// +// +// t +// ( h1 . f1 ) : exact ; .FieldMatchs +// actions { a ; ( b ; .ActionNameItems ) } +// .TableOptionals +// T:List +// . +//
+// +// +// +// ingress +// apply ( t ) { .HitMissCases } .ControlStatements +// +// +// SetItem ( ingress ) +// .Set +// +// .List +// ("$rule" |-> (_:K)) ("$table" |-> (_:K)) ("$action" |-> (_:K)) ("$miss" |-> (_:K)) +// +// _:List +// _:List +// +// +// .Set +// +// SetItem ( start ) +// SetItem ( h1 ) +// +// ListItem ( h1 ) +// +// +// 0 +// _ +// _ +// _ +// +// +// +// L:PacketList +// @nilPacketList +// +// +//ensures vars(ListItem(L) ListItem(T)) + + +//start of execution (p0) +rule + + @exec + +
+ %standard_metadata_t + .Map + ingress_port : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( egress_spec : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+
+ h_t + "$fixed_width" |-> 16 + f1 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( f2 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+ + .Map + .Bag + .Bag + .Bag + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> @undef egress_spec |-> @undef + + + false + false + h_t + h1 + .Map + + + + .Bag + + ListItem ( h1 ) ListItem ( standard_metadata ) + .Map + + + start + ( extract ( h1 ) ; .ExtractOrSetStatements ) return ingress ; + + + .Bag + .Bag + .Set + .Bag + .Map + + + b + .ParamList + modify_field ( ( standard_metadata . egress_spec ) , ( #token("2","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements + + + a + n , .ParamList + modify_field ( ( h1 . f2 ) , ( n , .Args ) ) ; ( modify_field ( ( standard_metadata . egress_spec ) , ( #token("1","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements ) + + + .Bag + .Bag + + + t + ( h1 . f1 ) : exact ; .FieldMatchs + actions { a ; ( b ; .ActionNameItems ) } + .TableOptionals + T:EntryList + D:DefaultEntry +
+ + + + ingress + apply ( t ) { .HitMissCases } .ControlStatements + + + SetItem ( ingress ) + .Set + + .List + ("$rule" |-> (_:K)) ("$table" |-> (_:K)) ("$action" |-> (_:K)) ("$miss" |-> (_:K)) + + _ + _ + + + .Set + + SetItem ( start ) + SetItem ( h1 ) + + ListItem ( h1 ) + + + 0 + _ + _ + _ + + + + I:PacketList + $nilPacketList + + +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #noUndefPacketList(I) +ensures vars(ListItem(I) ListItem(T) ListItem(D)) + +//loop over packets (p1) +rule + + @nextPacket + +
+ %standard_metadata_t + .Map + ingress_port : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( egress_spec : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+
+ h_t + "$fixed_width" |-> 16 + f1 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( f2 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+ + .Map + .Bag + .Bag + .Bag + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> _:Val egress_spec |-> _:Val + + + _ + false + h_t + h1 + _:Map + + + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> @undef egress_spec |-> @undef + + + false + false + h_t + h1 + .Map + + + ListItem ( h1 ) ListItem ( standard_metadata ) + .Map + + + start + ( extract ( h1 ) ; .ExtractOrSetStatements ) return ingress ; + + + .Bag + .Bag + .Set + .Bag + .Map + + + b + .ParamList + modify_field ( ( standard_metadata . egress_spec ) , ( #token("2","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements + + + a + n , .ParamList + modify_field ( ( h1 . f2 ) , ( n , .Args ) ) ; ( modify_field ( ( standard_metadata . egress_spec ) , ( #token("1","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements ) + + + .Bag + .Bag + + + t + ( h1 . f1 ) : exact ; .FieldMatchs + actions { a ; ( b ; .ActionNameItems ) } + .TableOptionals + T:EntryList + D:DefaultEntry +
+ + + + ingress + apply ( t ) { .HitMissCases } .ControlStatements + + + SetItem ( ingress ) + .Set + + .List + ("$rule" |-> (_:K)) ("$table" |-> (_:K)) ("$action" |-> (_:K)) ("$miss" |-> (_:K)) + + _:Vals + _:Vals + + + .Set + + SetItem ( start ) + SetItem ( h1 ) + + ListItem ( h1 ) + + + _ + _ + _ + _ + + + + I:PacketList + O:PacketList + + +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #noUndefPacketList(I) //andBool #noUndefPacketList(O) +ensures vars(ListItem(T) ListItem(I) ListItem(O) ListItem(D)) + +//experience: the order of elements in cell fragments (e.g instances) must be the same (associative matching does not work in this case) + +//loop over entries (p2) +rule + + @checkNextRule ( ( h1 . f1 ) : exact ; .FieldMatchs , C:EntryList ) ~> @setCrnt ( "$table" , . ) ~> @checkNextAppSelCase ( .HitMissCases ) ~> .ControlStatements ~> @egress ~> @txenPacket ~> @nextPacket + +
+ %standard_metadata_t + .Map + ingress_port : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( egress_spec : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+
+ h_t + "$fixed_width" |-> 16 + f1 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( f2 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+ + .Map + .Bag + .Bag + .Bag + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> @val ( _ , 32 , false ) egress_spec |-> E:Val + + + true + false + h_t + h1 + //f2 |-> @val ( F2:Int , 8 , false ) f1 |-> @val ( F1:Int , 8 , false ) //we don't check width during extraction for packets given using @vals + //f2 |-> @val ( F2:Int , _ , _ ) f1 |-> @val ( F1:Int , _ , _ ) // because impp assumes certain width, so we adjustVal during extraction anyway + f2 |-> @val ( F2:Int , 8 , false ) f1 |-> @val ( F1:Int , 8 , false ) + + + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> @undef egress_spec |-> @undef + + + false + false + h_t + h1 + .Map + + + ListItem ( h1 ) ListItem ( standard_metadata ) + .Map + + + start + ( extract ( h1 ) ; .ExtractOrSetStatements ) return ingress ; + + + .Bag + .Bag + .Set + .Bag + .Map + + + b + .ParamList + modify_field ( ( standard_metadata . egress_spec ) , ( #token("2","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements + + + a + n , .ParamList + modify_field ( ( h1 . f2 ) , ( n , .Args ) ) ; ( modify_field ( ( standard_metadata . egress_spec ) , ( #token("1","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements ) + + + .Bag + .Bag + + + t + ( h1 . f1 ) : exact ; .FieldMatchs + actions { a ; ( b ; .ActionNameItems ) } + .TableOptionals + T:EntryList + D:DefaultEntry +
+ + + + ingress + apply ( t ) { .HitMissCases } .ControlStatements + + + SetItem ( ingress ) + .Set + + .List + ("$rule" |-> (_:K)) ("$table" |-> (_:K)) ("$action" |-> (_:K)) ("$miss" |-> (_:K)) + + PL:Vals + @nil + + + .Set + + SetItem ( start ) + SetItem ( h1 ) + + ListItem ( h1 ) + + + _ + _ + _ + _ + + + + I:PacketList + O:PacketList + + +//ListItem(#egressToInt(E)) +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #wellDefTable(C) andBool #noUndefPacketList(I) //andBool #noUndefPacket(PL) //andBool #noUndefPacketList(O) +ensures vars(ListItem(I) ListItem(O) ListItem(T) ListItem(C) ListItem(F1) ListItem(F2) ListItem(#egressVal2Int(E)) ListItem(D) ListItem(PL)) + + +// p? +// loop over payload data +rule + + @addPayload ~> @txenPacket ~> @nextPacket + +
+ %standard_metadata_t + .Map + ingress_port : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( egress_spec : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+
+ h_t + "$fixed_width" |-> 16 + f1 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( f2 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+ + .Map + .Bag + .Bag + .Bag + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> @val ( _ , 32 , false ) egress_spec |-> E:Val + + + true + false + h_t + h1 + //f2 |-> @val ( F2:Int , 8 , false ) f1 |-> @val ( F1:Int , 8 , false ) //we don't check width during extraction for packets given using @vals + f2 |-> _:Val f1 |-> _:Val + + + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> @undef egress_spec |-> @undef + + + false + false + h_t + h1 + .Map + + + ListItem ( h1 ) ListItem ( standard_metadata ) + .Map + + + start + ( extract ( h1 ) ; .ExtractOrSetStatements ) return ingress ; + + + .Bag + .Bag + .Set + .Bag + .Map + + + b + .ParamList + modify_field ( ( standard_metadata . egress_spec ) , ( #token("2","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements + + + a + n , .ParamList + modify_field ( ( h1 . f2 ) , ( n , .Args ) ) ; ( modify_field ( ( standard_metadata . egress_spec ) , ( #token("1","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements ) + + + .Bag + .Bag + + + t + ( h1 . f1 ) : exact ; .FieldMatchs + actions { a ; ( b ; .ActionNameItems ) } + .TableOptionals + T:EntryList + D:DefaultEntry +
+ + + + ingress + apply ( t ) { .HitMissCases } .ControlStatements + + + SetItem ( ingress ) + .Set + + .List + ("$rule" |-> (_:K)) ("$table" |-> (_:K)) ("$action" |-> (_:K)) ("$miss" |-> (_:K)) + + PL:Vals + PO:Vals + + + .Set + + SetItem ( start ) + SetItem ( h1 ) + + ListItem ( h1 ) + + + _ + _ + _ + _ + + + + I:PacketList + O:PacketList + + +//ListItem(#egressToInt(E)) +requires #wellDefTable(T) andBool #wellDefDefaultAction(D) andBool #noUndefPacketList(I) //andBool #noUndefPacket(PL) +ensures vars(ListItem(I) ListItem(O) ListItem(T) ListItem(#egressVal2Int(E)) ListItem(PO) ListItem(PL) ListItem(D)) + + +//end (p3) +rule + + @end + +
+ %standard_metadata_t + .Map + ingress_port : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( egress_spec : #token("32","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+
+ h_t + "$fixed_width" |-> 16 + f1 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; ( f2 : #token("8","DecimalValueToken@VALUE-SYNTAX") ( .FieldMods ) ; .FieldDecs ) +
+ + .Map + .Bag + .Bag + .Bag + + + true + true + %standard_metadata_t + standard_metadata + ingress_port |-> _:Val egress_spec |-> _:Val + + + _ + false + h_t + h1 + _ + + + _ + ListItem ( h1 ) ListItem ( standard_metadata ) + .Map + + + start + ( extract ( h1 ) ; .ExtractOrSetStatements ) return ingress ; + + + .Bag + .Bag + .Set + .Bag + .Map + + + b + .ParamList + modify_field ( ( standard_metadata . egress_spec ) , ( #token("2","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements + + + a + n , .ParamList + modify_field ( ( h1 . f2 ) , ( n , .Args ) ) ; ( modify_field ( ( standard_metadata . egress_spec ) , ( #token("1","DecimalValueToken@VALUE-SYNTAX") , .Args ) ) ; .ActionStatements ) + + + .Bag + .Bag + + + t + ( h1 . f1 ) : exact ; .FieldMatchs + actions { a ; ( b ; .ActionNameItems ) } + .TableOptionals + _ + _ +
+ + + + ingress + apply ( t ) { .HitMissCases } .ControlStatements + + + SetItem ( ingress ) + .Set + + .List + ("$rule" |-> (_:K)) ("$table" |-> (_:K)) ("$action" |-> (_:K)) ("$miss" |-> (_:K)) + + _ + _ + + + .Set + + SetItem ( start ) + SetItem ( h1 ) + + ListItem ( h1 ) + + + _ + _ + _ + _ + + + + $nilPacketList + O:PacketList + + +ensures vars(ListItem(O) ListItem(0)) +[trusted] +endmodule + + + + + + + + + diff --git a/tranlation-validation/simple/kkompile.sh b/tranlation-validation/simple/kkompile.sh new file mode 100755 index 0000000..0e8a491 --- /dev/null +++ b/tranlation-validation/simple/kkompile.sh @@ -0,0 +1,4 @@ +#!/bin/bash -x +kompile --syntax-module P4-SYNTAX p4-semantics.k +kompile imppp.k +kompile common.k diff --git a/tranlation-validation/simple/psrun13.sh b/tranlation-validation/simple/psrun13.sh new file mode 100755 index 0000000..fb51ab2 --- /dev/null +++ b/tranlation-validation/simple/psrun13.sh @@ -0,0 +1 @@ +keq -v --debug --def0 common-kompiled --def1 p4-semantics-kompiled --def2 imppp-kompiled --prove1 13p4-5syncpoints-spec.k --prove2 13imppp-5syncpoints-spec.k --smt_prelude ../../verification/load-balancer/list.smt2