search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Problem with symbolic execution #2299

Open kheradmand opened 7 years ago

kheradmand commented 7 years ago

For my P4 semantics, I use string of 0s and 1s as input and the rules convert parts of this string to integer using String2Base. Concrete interpretation works fine but if I introduce a symbolic string instead of a concrete one, then I get some errors. I was wondering if this errors are expected or it is a bug. At the current moment I just want to know whether this error is caused by my use of string and string functions or it is because of something else?

One step before the error happens:

<T> <k> ( String2Base ( substrString ( V0 , 96 , 112 ) , 2 ) ==K 2048 ) ~> #freezer@if_@then_@else_1 ( return parse_ipv4 ; , @select ( @cons ( @val ( String2Base ( substrString ( V0 , 96 , 112 ) , 2 ) , 16 , false ) , @nil ) , default : ingress ;  .CaseEntries ) ) ~> @egress </k> <headers> <header> <name> %standard_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> ingress_port : 32 ( .FieldMods ) ;  ( egress_spec : 32 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> <header> <name> ingress_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> vrf : 12 ( .FieldMods ) ;  ( bd : 16 ( .FieldMods ) ;  ( nexthop_index : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> <header> <name> ipv4_t </name> <opts> .HeaderOptionals </opts> <fields> version : 4 ( .FieldMods ) ;  ( ihl : 4 ( .FieldMods ) ;  ( diffserv : 8 ( .FieldMods ) ;  ( totalLen : 16 ( .FieldMods ) ;  ( identification : 16 ( .FieldMods ) ;  ( flags : 3 ( .FieldMods ) ;  ( fragOffset : 13 ( .FieldMods ) ;  ( ttl : 8 ( .FieldMods ) ;  ( protocol : 8 ( .FieldMods ) ;  ( hdrChecksum : 16 ( .FieldMods ) ;  ( srcAddr : 32 ( .FieldMods ) ;  ( dstAddr : 32 ( .FieldMods ) ;  .FieldDecs ) ) ) ) ) ) ) ) ) ) ) </fields> </header> <header> <name> ethernet_t </name> <opts> .HeaderOptionals </opts> <fields> dstAddr : 48 ( .FieldMods ) ;  ( srcAddr : 48 ( .FieldMods ) ;  ( etherType : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> </headers> <instances> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> %standard_metadata_t </typeName> <name> standard_metadata </name> <fieldVals> ingress_port |-> @val ( 1 , 32 , false ) egress_spec |-> @val ( 0 , 32 , true ) </fieldVals> </instance> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> ingress_metadata_t </typeName> <name> ingress_metadata </name> <fieldVals> bd |-> @val ( 0 , 0 , false ) nexthop_index |-> @val ( 0 , 0 , false ) vrf |-> @val ( 0 , 0 , false ) </fieldVals> </instance> <instance> <valid> false </valid> <metadata> false </metadata> <typeName> ipv4_t </typeName> <name> ipv4 </name> <fieldVals> .Map </fieldVals> </instance> <instance> <valid> true </valid> <metadata> false </metadata> <typeName> ethernet_t </typeName> <name> ethernet </name> <fieldVals> etherType |-> @val ( String2Base ( substrString ( V0 , 96 , 112 ) , 2 ) , 16 , false ) srcAddr |-> @val ( String2Base ( substrString ( V0 , 48 , 96 ) , 2 ) , 48 , false ) dstAddr |-> @val ( String2Base ( substrString ( V0 , 0 , 48 ) , 2 ) , 48 , false ) </fieldVals> </instance> </instances> <parserStates> <state> <name> parse_ipv4 </name> <body> ( extract ( ipv4 ) ; .ExtractOrSetStatements ) return ingress ; </body> </state> <state> <name> parse_ethernet </name> <body> ( extract ( ethernet ) ; .ExtractOrSetStatements ) return select ( ( latest . etherType ) , .FieldOrDataRefs ) { ( 0x0800 , .ValueOrMaskeds ) : parse_ipv4 ;  ( default : ingress ;  .CaseEntries ) } </body> </state> <state> <name> start </name> <body> .ExtractOrSetStatements return parse_ethernet ; </body> </state> </parserStates> <actions> <action> <name> rewrite_src_dst_mac </name> <params> smac , ( dmac , .ParamList ) </params> <body> modify_field ( ( ethernet . srcAddr ) , ( smac , .Args ) ) ;  ( modify_field ( ( ethernet . dstAddr ) , ( dmac , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_egress_details </name> <params> egress_spec , .ParamList </params> <body> modify_field ( ( standard_metadata . egress_spec ) , ( egress_spec , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> fib_hit_nexthop </name> <params> nexthop_index , .ParamList </params> <body> modify_field ( ( ingress_metadata . nexthop_index ) , ( nexthop_index , .Args ) ) ;  ( subtract_from_field ( ( ipv4 . ttl ) , ( 1 , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_vrf </name> <params> vrf , .ParamList </params> <body> modify_field ( ( ingress_metadata . vrf ) , ( vrf , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> set_bd </name> <params> bd , .ParamList </params> <body> modify_field ( ( ingress_metadata . bd ) , ( bd , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> on_miss </name> <params> .ParamList </params> <body> .ActionStatements </body> </action> </actions> <tables> <table> <name> rewrite_mac </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( rewrite_src_dst_mac ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1103823438081 , 0 , false ) ) ListItem ( @val ( 4311810305 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1108135248386 , 0 , false ) ) ListItem ( @val ( 8623620610 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1112447058691 , 0 , false ) ) ListItem ( @val ( 12935430915 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1116758868996 , 0 , false ) ) ListItem ( @val ( 17247241220 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> nexthop </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( set_egress_details ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 2 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 4 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> ipv4_fib_lpm </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : lpm ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 16384 ;  .TableOptionals </opts> <rules> .List </rules> </table> <table> <name> ipv4_fib </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : exact ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 131072 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 3232235520 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 167772160 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> bd </name> <reads> ( ingress_metadata . bd ) : exact ;  .FieldMatchs </reads> <acts> actions { set_vrf ;  .ActionNameItems } </acts> <opts> size : 65536 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> port_mapping </name> <reads> ( standard_metadata . ingress_port ) : exact ;  .FieldMatchs </reads> <acts> actions { set_bd ;  .ActionNameItems } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </rules> </table> </tables> <controlFlows> <control> <name> egress </name> <body> apply ( rewrite_mac ) { .HitMissCases }  .ControlStatements </body> </control> <control> <name> ingress </name> <body> ( if ( valid ( ipv4 ) ) { apply ( port_mapping ) { .HitMissCases }  ( apply ( bd ) { .HitMissCases }  ( apply ( ipv4_fib ) { ( on_miss { apply ( ipv4_fib_lpm ) { .HitMissCases }  .ControlStatements } )  .ActionCases }  ( apply ( nexthop ) { .HitMissCases }  .ControlStatements ) ) ) } else { .ControlStatements } )  .ControlStatements </body> </control> </controlFlows> <cfset> SetItem ( ingress ) SetItem ( egress ) </cfset> <frameStack> .List </frameStack> <packet> V0 </packet> <packetout> . </packetout> <parser> <graph> <marked> SetItem ( ipv4 ) SetItem ( ethernet ) </marked> <dporder> ListItem ( ethernet ) ListItem ( ipv4 ) </dporder> </graph> <index> 112 </index> <lastExt> ethernet </lastExt> </parser> </T>

The next step:

(error "line 5 column 27: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 5 column 27: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 5 column 27: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
<T> <k> V0 ~> #freezer_==_0 ( V1 ) ~> #freezer@if_@then_@else_1 ( return parse_ipv4 ; , @select ( @cons ( @val ( String2Base ( substrString ( V2 , 96 , 112 ) , 2 ) , 16 , false ) , @nil ) , default : ingress ;  .CaseEntries ) ) ~> @egress </k> <headers> <header> <name> %standard_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> ingress_port : 32 ( .FieldMods ) ;  ( egress_spec : 32 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> <header> <name> ingress_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> vrf : 12 ( .FieldMods ) ;  ( bd : 16 ( .FieldMods ) ;  ( nexthop_index : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> <header> <name> ipv4_t </name> <opts> .HeaderOptionals </opts> <fields> version : 4 ( .FieldMods ) ;  ( ihl : 4 ( .FieldMods ) ;  ( diffserv : 8 ( .FieldMods ) ;  ( totalLen : 16 ( .FieldMods ) ;  ( identification : 16 ( .FieldMods ) ;  ( flags : 3 ( .FieldMods ) ;  ( fragOffset : 13 ( .FieldMods ) ;  ( ttl : 8 ( .FieldMods ) ;  ( protocol : 8 ( .FieldMods ) ;  ( hdrChecksum : 16 ( .FieldMods ) ;  ( srcAddr : 32 ( .FieldMods ) ;  ( dstAddr : 32 ( .FieldMods ) ;  .FieldDecs ) ) ) ) ) ) ) ) ) ) ) </fields> </header> <header> <name> ethernet_t </name> <opts> .HeaderOptionals </opts> <fields> dstAddr : 48 ( .FieldMods ) ;  ( srcAddr : 48 ( .FieldMods ) ;  ( etherType : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> </headers> <instances> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> %standard_metadata_t </typeName> <name> standard_metadata </name> <fieldVals> ingress_port |-> @val ( 1 , 32 , false ) egress_spec |-> @val ( 0 , 32 , true ) </fieldVals> </instance> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> ingress_metadata_t </typeName> <name> ingress_metadata </name> <fieldVals> bd |-> @val ( 0 , 0 , false ) nexthop_index |-> @val ( 0 , 0 , false ) vrf |-> @val ( 0 , 0 , false ) </fieldVals> </instance> <instance> <valid> false </valid> <metadata> false </metadata> <typeName> ipv4_t </typeName> <name> ipv4 </name> <fieldVals> .Map </fieldVals> </instance> <instance> <valid> true </valid> <metadata> false </metadata> <typeName> ethernet_t </typeName> <name> ethernet </name> <fieldVals> etherType |-> @val ( String2Base ( substrString ( V2 , 96 , 112 ) , 2 ) , 16 , false ) srcAddr |-> @val ( String2Base ( substrString ( V2 , 48 , 96 ) , 2 ) , 48 , false ) dstAddr |-> @val ( String2Base ( substrString ( V2 , 0 , 48 ) , 2 ) , 48 , false ) </fieldVals> </instance> </instances> <parserStates> <state> <name> parse_ipv4 </name> <body> ( extract ( ipv4 ) ; .ExtractOrSetStatements ) return ingress ; </body> </state> <state> <name> parse_ethernet </name> <body> ( extract ( ethernet ) ; .ExtractOrSetStatements ) return select ( ( latest . etherType ) , .FieldOrDataRefs ) { ( 0x0800 , .ValueOrMaskeds ) : parse_ipv4 ;  ( default : ingress ;  .CaseEntries ) } </body> </state> <state> <name> start </name> <body> .ExtractOrSetStatements return parse_ethernet ; </body> </state> </parserStates> <actions> <action> <name> rewrite_src_dst_mac </name> <params> smac , ( dmac , .ParamList ) </params> <body> modify_field ( ( ethernet . srcAddr ) , ( smac , .Args ) ) ;  ( modify_field ( ( ethernet . dstAddr ) , ( dmac , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_egress_details </name> <params> egress_spec , .ParamList </params> <body> modify_field ( ( standard_metadata . egress_spec ) , ( egress_spec , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> fib_hit_nexthop </name> <params> nexthop_index , .ParamList </params> <body> modify_field ( ( ingress_metadata . nexthop_index ) , ( nexthop_index , .Args ) ) ;  ( subtract_from_field ( ( ipv4 . ttl ) , ( 1 , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_vrf </name> <params> vrf , .ParamList </params> <body> modify_field ( ( ingress_metadata . vrf ) , ( vrf , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> set_bd </name> <params> bd , .ParamList </params> <body> modify_field ( ( ingress_metadata . bd ) , ( bd , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> on_miss </name> <params> .ParamList </params> <body> .ActionStatements </body> </action> </actions> <tables> <table> <name> rewrite_mac </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( rewrite_src_dst_mac ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1103823438081 , 0 , false ) ) ListItem ( @val ( 4311810305 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1108135248386 , 0 , false ) ) ListItem ( @val ( 8623620610 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1112447058691 , 0 , false ) ) ListItem ( @val ( 12935430915 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1116758868996 , 0 , false ) ) ListItem ( @val ( 17247241220 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> nexthop </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( set_egress_details ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 2 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 4 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> ipv4_fib_lpm </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : lpm ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 16384 ;  .TableOptionals </opts> <rules> .List </rules> </table> <table> <name> ipv4_fib </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : exact ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 131072 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 3232235520 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 167772160 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> bd </name> <reads> ( ingress_metadata . bd ) : exact ;  .FieldMatchs </reads> <acts> actions { set_vrf ;  .ActionNameItems } </acts> <opts> size : 65536 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> port_mapping </name> <reads> ( standard_metadata . ingress_port ) : exact ;  .FieldMatchs </reads> <acts> actions { set_bd ;  .ActionNameItems } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </rules> </table> </tables> <controlFlows> <control> <name> egress </name> <body> apply ( rewrite_mac ) { .HitMissCases }  .ControlStatements </body> </control> <control> <name> ingress </name> <body> ( if ( valid ( ipv4 ) ) { apply ( port_mapping ) { .HitMissCases }  ( apply ( bd ) { .HitMissCases }  ( apply ( ipv4_fib ) { ( on_miss { apply ( ipv4_fib_lpm ) { .HitMissCases }  .ControlStatements } )  .ActionCases }  ( apply ( nexthop ) { .HitMissCases }  .ControlStatements ) ) ) } else { .ControlStatements } )  .ControlStatements </body> </control> </controlFlows> <cfset> SetItem ( ingress ) SetItem ( egress ) </cfset> <frameStack> .List </frameStack> <packet> V2 </packet> <packetout> . </packetout> <parser> <graph> <marked> SetItem ( ipv4 ) SetItem ( ethernet ) </marked> <dporder> ListItem ( ethernet ) ListItem ( ipv4 ) </dporder> </graph> <index> 112 </index> <lastExt> ethernet </lastExt> </parser> </T>
[Warning] Critical: failed to translate smtlib expression:
(declare-sort BoolExpr)
(declare-fun _2211 () Bool)
(declare-fun _2213 () Bool)
(declare-fun _2212 () BoolExpr)
(assert (and (= _2211 _2212) (= _2213 false)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort BoolExpr)
(declare-fun _2214 () Bool)
(declare-fun _2216 () Bool)
(declare-fun _2215 () BoolExpr)
(assert (and (= _2214 _2215) (= _2216 false)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort BoolExpr)
(declare-fun _2231 () Bool)
(declare-fun _2233 () Bool)
(declare-fun _2232 () BoolExpr)
(assert (and (= _2231 _2232) (= _2233 false)))

And the step after that:

(error "line 5 column 27: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 5 column 27: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 5 column 27: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
java.lang.AssertionError
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.getSubstitution(ConjunctiveFormula.java:534)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:417)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.addUnification(FastRuleMatcher.java:512)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:228)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:438)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:164)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:105)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:86)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:148)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:65)
    at org.kframework.krun.KRun.run(KRun.java:103)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
    at org.kframework.main.Main.runApplication(Main.java:414)
    at org.kframework.main.Main.runApplication(Main.java:265)
    at org.kframework.main.Main.main(Main.java:74)
java.lang.AssertionError
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.getSubstitution(ConjunctiveFormula.java:534)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:417)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.addUnification(FastRuleMatcher.java:512)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:228)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:438)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:164)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:105)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:86)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:148)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:65)
    at org.kframework.krun.KRun.run(KRun.java:103)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
    at org.kframework.main.Main.runApplication(Main.java:414)
    at org.kframework.main.Main.runApplication(Main.java:265)
    at org.kframework.main.Main.main(Main.java:74)
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
[Warning] Critical: failed to translate smtlib expression:
(declare-sort BoolExpr)
(declare-fun _2211 () Bool)
(declare-fun _2213 () Bool)
(declare-fun _2212 () BoolExpr)
(assert (and (= _2211 _2212) (= _2213 false)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort BoolExpr)
(declare-fun _2214 () Bool)
(declare-fun _2216 () Bool)
(declare-fun _2215 () BoolExpr)
(assert (and (= _2214 _2215) (= _2216 false)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort BoolExpr)
(declare-fun _2231 () Bool)
(declare-fun _2233 () Bool)
(declare-fun _2232 () BoolExpr)
(assert (and (= _2231 _2232) (= _2233 false)))

@daejunpark

kheradmand commented 7 years ago

It seems that it is not related to packets being string. I changed the packets structure and still get this kind of errors:

An step before error:

<T> <k> ( V0 ==K 2048 ) ~> #freezer@if_@then_@else_1 ( return parse_ipv4 ; , @select ( @cons ( @val ( V0 , V1 , V2 ) , @nil ) , default : ingress ;  .CaseEntries ) ) ~> @egress </k> <headers> <header> <name> %standard_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> ingress_port : 32 ( .FieldMods ) ;  ( egress_spec : 32 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> <header> <name> ingress_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> vrf : 12 ( .FieldMods ) ;  ( bd : 16 ( .FieldMods ) ;  ( nexthop_index : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> <header> <name> ipv4_t </name> <opts> .HeaderOptionals </opts> <fields> version : 4 ( .FieldMods ) ;  ( ihl : 4 ( .FieldMods ) ;  ( diffserv : 8 ( .FieldMods ) ;  ( totalLen : 16 ( .FieldMods ) ;  ( identification : 16 ( .FieldMods ) ;  ( flags : 3 ( .FieldMods ) ;  ( fragOffset : 13 ( .FieldMods ) ;  ( ttl : 8 ( .FieldMods ) ;  ( protocol : 8 ( .FieldMods ) ;  ( hdrChecksum : 16 ( .FieldMods ) ;  ( srcAddr : 32 ( .FieldMods ) ;  ( dstAddr : 32 ( .FieldMods ) ;  .FieldDecs ) ) ) ) ) ) ) ) ) ) ) </fields> </header> <header> <name> ethernet_t </name> <opts> .HeaderOptionals </opts> <fields> dstAddr : 48 ( .FieldMods ) ;  ( srcAddr : 48 ( .FieldMods ) ;  ( etherType : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> </headers> <instances> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> %standard_metadata_t </typeName> <name> standard_metadata </name> <fieldVals> ingress_port |-> @val ( 1 , 32 , false ) egress_spec |-> @val ( 0 , 32 , true ) </fieldVals> </instance> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> ingress_metadata_t </typeName> <name> ingress_metadata </name> <fieldVals> bd |-> @val ( 0 , 0 , false ) nexthop_index |-> @val ( 0 , 0 , false ) vrf |-> @val ( 0 , 0 , false ) </fieldVals> </instance> <instance> <valid> false </valid> <metadata> false </metadata> <typeName> ipv4_t </typeName> <name> ipv4 </name> <fieldVals> .Map </fieldVals> </instance> <instance> <valid> true </valid> <metadata> false </metadata> <typeName> ethernet_t </typeName> <name> ethernet </name> <fieldVals> etherType |-> @val ( V0 , V1 , V2 ) srcAddr |-> @val ( V6 , V7 , V8 ) dstAddr |-> @val ( V3 , V4 , V5 ) </fieldVals> </instance> </instances> <parserStates> <state> <name> parse_ipv4 </name> <body> ( extract ( ipv4 ) ; .ExtractOrSetStatements ) return ingress ; </body> </state> <state> <name> parse_ethernet </name> <body> ( extract ( ethernet ) ; .ExtractOrSetStatements ) return select ( ( latest . etherType ) , .FieldOrDataRefs ) { ( 0x0800 , .ValueOrMaskeds ) : parse_ipv4 ;  ( default : ingress ;  .CaseEntries ) } </body> </state> <state> <name> start </name> <body> .ExtractOrSetStatements return parse_ethernet ; </body> </state> </parserStates> <actions> <action> <name> rewrite_src_dst_mac </name> <params> smac , ( dmac , .ParamList ) </params> <body> modify_field ( ( ethernet . srcAddr ) , ( smac , .Args ) ) ;  ( modify_field ( ( ethernet . dstAddr ) , ( dmac , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_egress_details </name> <params> egress_spec , .ParamList </params> <body> modify_field ( ( standard_metadata . egress_spec ) , ( egress_spec , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> fib_hit_nexthop </name> <params> nexthop_index , .ParamList </params> <body> modify_field ( ( ingress_metadata . nexthop_index ) , ( nexthop_index , .Args ) ) ;  ( subtract_from_field ( ( ipv4 . ttl ) , ( 1 , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_vrf </name> <params> vrf , .ParamList </params> <body> modify_field ( ( ingress_metadata . vrf ) , ( vrf , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> set_bd </name> <params> bd , .ParamList </params> <body> modify_field ( ( ingress_metadata . bd ) , ( bd , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> on_miss </name> <params> .ParamList </params> <body> .ActionStatements </body> </action> </actions> <tables> <table> <name> rewrite_mac </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( rewrite_src_dst_mac ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1103823438081 , 0 , false ) ) ListItem ( @val ( 4311810305 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1108135248386 , 0 , false ) ) ListItem ( @val ( 8623620610 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1112447058691 , 0 , false ) ) ListItem ( @val ( 12935430915 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1116758868996 , 0 , false ) ) ListItem ( @val ( 17247241220 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> nexthop </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( set_egress_details ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 2 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 4 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> ipv4_fib_lpm </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : lpm ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 16384 ;  .TableOptionals </opts> <rules> .List </rules> </table> <table> <name> ipv4_fib </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : exact ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 131072 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 3232235520 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 167772160 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> bd </name> <reads> ( ingress_metadata . bd ) : exact ;  .FieldMatchs </reads> <acts> actions { set_vrf ;  .ActionNameItems } </acts> <opts> size : 65536 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> port_mapping </name> <reads> ( standard_metadata . ingress_port ) : exact ;  .FieldMatchs </reads> <acts> actions { set_bd ;  .ActionNameItems } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </rules> </table> </tables> <controlFlows> <control> <name> egress </name> <body> apply ( rewrite_mac ) { .HitMissCases }  .ControlStatements </body> </control> <control> <name> ingress </name> <body> ( if ( valid ( ipv4 ) ) { apply ( port_mapping ) { .HitMissCases }  ( apply ( bd ) { .HitMissCases }  ( apply ( ipv4_fib ) { ( on_miss { apply ( ipv4_fib_lpm ) { .HitMissCases }  .ControlStatements } )  .ActionCases }  ( apply ( nexthop ) { .HitMissCases }  .ControlStatements ) ) ) } else { .ControlStatements } )  .ControlStatements </body> </control> </controlFlows> <cfset> SetItem ( ingress ) SetItem ( egress ) </cfset> <frameStack> .List </frameStack> <packet> V9 </packet> <packetout> . </packetout> <parser> <graph> <marked> SetItem ( ipv4 ) SetItem ( ethernet ) </marked> <dporder> ListItem ( ethernet ) ListItem ( ipv4 ) </dporder> </graph> <index> 3 </index> <lastExt> ethernet </lastExt> </parser> </T>

The next step;

(error "line 12 column 52: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 12 column 52: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 12 column 52: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
<T> <k> V0 ~> #freezer_==_0 ( V1 ) ~> #freezer@if_@then_@else_1 ( return parse_ipv4 ; , @select ( @cons ( @val ( V2 , V3 , V4 ) , @nil ) , default : ingress ;  .CaseEntries ) ) ~> @egress </k> <headers> <header> <name> %standard_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> ingress_port : 32 ( .FieldMods ) ;  ( egress_spec : 32 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> <header> <name> ingress_metadata_t </name> <opts> .HeaderOptionals </opts> <fields> vrf : 12 ( .FieldMods ) ;  ( bd : 16 ( .FieldMods ) ;  ( nexthop_index : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> <header> <name> ipv4_t </name> <opts> .HeaderOptionals </opts> <fields> version : 4 ( .FieldMods ) ;  ( ihl : 4 ( .FieldMods ) ;  ( diffserv : 8 ( .FieldMods ) ;  ( totalLen : 16 ( .FieldMods ) ;  ( identification : 16 ( .FieldMods ) ;  ( flags : 3 ( .FieldMods ) ;  ( fragOffset : 13 ( .FieldMods ) ;  ( ttl : 8 ( .FieldMods ) ;  ( protocol : 8 ( .FieldMods ) ;  ( hdrChecksum : 16 ( .FieldMods ) ;  ( srcAddr : 32 ( .FieldMods ) ;  ( dstAddr : 32 ( .FieldMods ) ;  .FieldDecs ) ) ) ) ) ) ) ) ) ) ) </fields> </header> <header> <name> ethernet_t </name> <opts> .HeaderOptionals </opts> <fields> dstAddr : 48 ( .FieldMods ) ;  ( srcAddr : 48 ( .FieldMods ) ;  ( etherType : 16 ( .FieldMods ) ;  .FieldDecs ) ) </fields> </header> </headers> <instances> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> %standard_metadata_t </typeName> <name> standard_metadata </name> <fieldVals> ingress_port |-> @val ( 1 , 32 , false ) egress_spec |-> @val ( 0 , 32 , true ) </fieldVals> </instance> <instance> <valid> true </valid> <metadata> true </metadata> <typeName> ingress_metadata_t </typeName> <name> ingress_metadata </name> <fieldVals> bd |-> @val ( 0 , 0 , false ) nexthop_index |-> @val ( 0 , 0 , false ) vrf |-> @val ( 0 , 0 , false ) </fieldVals> </instance> <instance> <valid> false </valid> <metadata> false </metadata> <typeName> ipv4_t </typeName> <name> ipv4 </name> <fieldVals> .Map </fieldVals> </instance> <instance> <valid> true </valid> <metadata> false </metadata> <typeName> ethernet_t </typeName> <name> ethernet </name> <fieldVals> etherType |-> @val ( V2 , V3 , V4 ) srcAddr |-> @val ( V8 , V9 , V10 ) dstAddr |-> @val ( V5 , V6 , V7 ) </fieldVals> </instance> </instances> <parserStates> <state> <name> parse_ipv4 </name> <body> ( extract ( ipv4 ) ; .ExtractOrSetStatements ) return ingress ; </body> </state> <state> <name> parse_ethernet </name> <body> ( extract ( ethernet ) ; .ExtractOrSetStatements ) return select ( ( latest . etherType ) , .FieldOrDataRefs ) { ( 0x0800 , .ValueOrMaskeds ) : parse_ipv4 ;  ( default : ingress ;  .CaseEntries ) } </body> </state> <state> <name> start </name> <body> .ExtractOrSetStatements return parse_ethernet ; </body> </state> </parserStates> <actions> <action> <name> rewrite_src_dst_mac </name> <params> smac , ( dmac , .ParamList ) </params> <body> modify_field ( ( ethernet . srcAddr ) , ( smac , .Args ) ) ;  ( modify_field ( ( ethernet . dstAddr ) , ( dmac , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_egress_details </name> <params> egress_spec , .ParamList </params> <body> modify_field ( ( standard_metadata . egress_spec ) , ( egress_spec , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> fib_hit_nexthop </name> <params> nexthop_index , .ParamList </params> <body> modify_field ( ( ingress_metadata . nexthop_index ) , ( nexthop_index , .Args ) ) ;  ( subtract_from_field ( ( ipv4 . ttl ) , ( 1 , .Args ) ) ;  .ActionStatements ) </body> </action> <action> <name> set_vrf </name> <params> vrf , .ParamList </params> <body> modify_field ( ( ingress_metadata . vrf ) , ( vrf , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> set_bd </name> <params> bd , .ParamList </params> <body> modify_field ( ( ingress_metadata . bd ) , ( bd , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> on_miss </name> <params> .ParamList </params> <body> .ActionStatements </body> </action> </actions> <tables> <table> <name> rewrite_mac </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( rewrite_src_dst_mac ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1103823438081 , 0 , false ) ) ListItem ( @val ( 4311810305 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1108135248386 , 0 , false ) ) ListItem ( @val ( 8623620610 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1112447058691 , 0 , false ) ) ListItem ( @val ( 12935430915 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( rewrite_src_dst_mac , $resolved ( ListItem ( @val ( 1116758868996 , 0 , false ) ) ListItem ( @val ( 17247241220 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> nexthop </name> <reads> ( ingress_metadata . nexthop_index ) : exact ;  .FieldMatchs </reads> <acts> actions { on_miss ;  ( set_egress_details ;  .ActionNameItems ) } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 2 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_egress_details , $resolved ( ListItem ( @val ( 4 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> ipv4_fib_lpm </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : lpm ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 16384 ;  .TableOptionals </opts> <rules> .List </rules> </table> <table> <name> ipv4_fib </name> <reads> ( ingress_metadata . vrf ) : exact ;  ( ( ipv4 . dstAddr ) : exact ;  .FieldMatchs ) </reads> <acts> actions { on_miss ;  ( fib_hit_nexthop ;  .ActionNameItems ) } </acts> <opts> size : 131072 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 3232235520 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 1 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 30 , 0 , false ) ) ListItem ( @val ( 167772160 , 0 , false ) ) ) , @call ( fib_hit_nexthop , $resolved ( ListItem ( @val ( 3 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> bd </name> <reads> ( ingress_metadata . bd ) : exact ;  .FieldMatchs </reads> <acts> actions { set_vrf ;  .ActionNameItems } </acts> <opts> size : 65536 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 10 , 0 , false ) ) ) , @call ( set_vrf , $resolved ( ListItem ( @val ( 30 , 0 , false ) ) ) ) ) ) </rules> </table> <table> <name> port_mapping </name> <reads> ( standard_metadata . ingress_port ) : exact ;  .FieldMatchs </reads> <acts> actions { set_bd ;  .ActionNameItems } </acts> <opts> size : 32768 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( $ctr ( ListItem ( @val ( 1 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 2 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 3 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) ListItem ( $rule ( $ctr ( ListItem ( @val ( 4 , 0 , false ) ) ) , @call ( set_bd , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </rules> </table> </tables> <controlFlows> <control> <name> egress </name> <body> apply ( rewrite_mac ) { .HitMissCases }  .ControlStatements </body> </control> <control> <name> ingress </name> <body> ( if ( valid ( ipv4 ) ) { apply ( port_mapping ) { .HitMissCases }  ( apply ( bd ) { .HitMissCases }  ( apply ( ipv4_fib ) { ( on_miss { apply ( ipv4_fib_lpm ) { .HitMissCases }  .ControlStatements } )  .ActionCases }  ( apply ( nexthop ) { .HitMissCases }  .ControlStatements ) ) ) } else { .ControlStatements } )  .ControlStatements </body> </control> </controlFlows> <cfset> SetItem ( ingress ) SetItem ( egress ) </cfset> <frameStack> .List </frameStack> <packet> V11 </packet> <packetout> . </packetout> <parser> <graph> <marked> SetItem ( ipv4 ) SetItem ( ethernet ) </marked> <dporder> ListItem ( ethernet ) ListItem ( ipv4 ) </dporder> </graph> <index> 3 </index> <lastExt> ethernet </lastExt> </parser> </T>
[Warning] Critical: failed to translate smtlib expression:
(declare-sort Val)
(declare-sort BoolExpr)
(declare-fun _1782 () Int)
(declare-fun _2255 () Val)
(declare-fun _2252 () Val)
(declare-fun _2251 () Val)
(declare-fun _2254 () Val)
(declare-fun _2248 () Val)
(declare-fun _2253 () Bool)
(declare-fun _2249 () Val)
(declare-fun _2250 () BoolExpr)
(assert (and (= _2248 _2249) (= (= _1782 2048) _2250) (= _2251 _2252) (= _2253
false) (= _2254 _2255)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort Val)
(declare-sort BoolExpr)
(declare-fun _1782 () Int)
(declare-fun _2263 () Val)
(declare-fun _2260 () Val)
(declare-fun _2259 () Val)
(declare-fun _2262 () Val)
(declare-fun _2256 () Val)
(declare-fun _2261 () Bool)
(declare-fun _2257 () Val)
(declare-fun _2258 () BoolExpr)
(assert (and (= _2256 _2257) (= (= _1782 2048) _2258) (= _2259 _2260) (= _2261
false) (= _2262 _2263)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort Val)
(declare-sort BoolExpr)
(declare-fun _1782 () Int)
(declare-fun _2283 () Bool)
(declare-fun _2285 () Val)
(declare-fun _2282 () Val)
(declare-fun _2281 () Val)
(declare-fun _2284 () Val)
(declare-fun _2278 () Val)
(declare-fun _2279 () Val)
(declare-fun _2280 () BoolExpr)
(assert (and (= _2278 _2279) (= (= _1782 2048) _2280) (= _2281 _2282) (= _2283
false) (= _2284 _2285)))

And the step after that:

(error "line 12 column 52: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 12 column 52: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
(error "line 12 column 52: invalid function application for =, sort mismatch on argument at position 2, expected Bool but given BoolExpr")
java.lang.AssertionError
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.getSubstitution(ConjunctiveFormula.java:534)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:417)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.addUnification(FastRuleMatcher.java:512)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:228)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:438)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:164)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:105)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:86)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:148)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:65)
    at org.kframework.krun.KRun.run(KRun.java:103)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
    at org.kframework.main.Main.runApplication(Main.java:414)
    at org.kframework.main.Main.runApplication(Main.java:265)
    at org.kframework.main.Main.main(Main.java:74)
java.lang.AssertionError
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.getSubstitution(ConjunctiveFormula.java:534)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:417)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.simplify(ConjunctiveFormula.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.addUnification(FastRuleMatcher.java:512)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:228)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchAssoc(FastRuleMatcher.java:438)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:323)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:271)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.match(FastRuleMatcher.java:315)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:107)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:164)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:105)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:86)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:148)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:65)
    at org.kframework.krun.KRun.run(KRun.java:103)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:68)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
    at org.kframework.main.Main.runApplication(Main.java:414)
    at org.kframework.main.Main.runApplication(Main.java:265)
    at org.kframework.main.Main.main(Main.java:74)
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
[Warning] Critical: failed to translate smtlib expression:
(declare-sort Val)
(declare-sort BoolExpr)
(declare-fun _1782 () Int)
(declare-fun _2255 () Val)
(declare-fun _2252 () Val)
(declare-fun _2251 () Val)
(declare-fun _2254 () Val)
(declare-fun _2248 () Val)
(declare-fun _2253 () Bool)
(declare-fun _2249 () Val)
(declare-fun _2250 () BoolExpr)
(assert (and (= _2248 _2249) (= (= _1782 2048) _2250) (= _2251 _2252) (= _2253
false) (= _2254 _2255)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort Val)
(declare-sort BoolExpr)
(declare-fun _1782 () Int)
(declare-fun _2263 () Val)
(declare-fun _2260 () Val)
(declare-fun _2259 () Val)
(declare-fun _2262 () Val)
(declare-fun _2256 () Val)
(declare-fun _2261 () Bool)
(declare-fun _2257 () Val)
(declare-fun _2258 () BoolExpr)
(assert (and (= _2256 _2257) (= (= _1782 2048) _2258) (= _2259 _2260) (= _2261
false) (= _2262 _2263)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort Val)
(declare-sort BoolExpr)
(declare-fun _1782 () Int)
(declare-fun _2283 () Bool)
(declare-fun _2285 () Val)
(declare-fun _2282 () Val)
(declare-fun _2281 () Val)
(declare-fun _2284 () Val)
(declare-fun _2278 () Val)
(declare-fun _2279 () Val)
(declare-fun _2280 () BoolExpr)
(assert (and (= _2278 _2279) (= (= _1782 2048) _2280) (= _2281 _2282) (= _2283
false) (= _2284 _2285)))
kheradmand commented 7 years ago

This is happening in commit 35df078e85e

kheradmand commented 7 years ago

@daejunpark It seems that the essence of the problem is this;

syntax KResult ::= Val | Bool
syntax Val ::= "@val" "(" Int "," Int "," Bool ")"
syntax BoolExpr ::=  Exp "==" Exp
syntax KItem ::=   K "%==" K [seqstrict]
syntax K ::= "@if" K /* Bool */ "@then" K "@else" K [strict(1)]           
syntax Exp ::= Val
syntax BoolExpr ::= Bool
rule V1:Val %== V2:Val => V1 == V2
rule @val(V1,_,_) == @val(V2,_,_) => V1 ==Int V2

With such a configuration:

@if @val(V0,V1,V2) %== @val(2048,0,false)  @then ...

The step after it is:

@val(V0,V1,V2) == @val(2048,0,false)

And the next step is:

V0 ==K 2048

And then I get the error

kheradmand commented 7 years ago

This one also has the same problem:

syntax KResult ::= Val | Bool
syntax Val ::= "@val" "(" Int "," Int "," Bool ")"
syntax KItem ::=   K "%==" K [seqstrict]
syntax K ::= "@if" K /* Bool */ "@then" K "@else" K [strict(1)]           
syntax Exp ::= Val
rule @val(V1,_,_) %== @val(V2,_,_) => V1 ==Int V2
kheradmand commented 7 years ago

thanks to @daejunpark, returning "unsat" when z3 throws such error seems to fix my problems for now

cos commented 7 years ago

is it safe/correct to return "unsat" on exception?

kheradmand commented 7 years ago

I don't know if it is generally safe/correct to do that, but for my very special case it seems to be correct

daejunpark commented 7 years ago

@cos It depends. But here we are interested in symbolic execution, and returning unsat on exception is not safe/correct. More generally, we have to consider a rule even if z3 returns unknown for satisfiability of the require constraint. Otherwise, we may miss some reachability behaviors.

But @kheradmand is ok to do it, since his goal is bug-finding not verification.

cos commented 7 years ago

@daejunpark, yep, I was thinking of symbolic execution.

@kheradmand, would there be any problem allowing the rule to apply instead? Would it significantly impact performance?

kheradmand commented 7 years ago

@cos in that case (which was the default behavior before I made the change I mentioned), I get to the assertionError that was mentioned in the first comment.

cos commented 7 years ago

@kheradmand, ok, I see.