search

kframework / k-legacy

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

"List [ Int ]" (sometimes) yields ListItem #2343

Open kheradmand opened 6 years ago

kheradmand commented 6 years ago

Hi I have the following configuration 

<T> <k> @val ( 0 , 14 , false ) ~> @deref ( sel_profile , 0 ) ~> @setCrntRule ( . ) ~> @setCrntTable ( . ) ~> .HitMissCases ~> .ControlStatements ~> @egress ~> @txenPacket ~> @nextPacket </k> <headers> <header> <name> %standard_metadata_t </name> <opts> .Map </opts> <fields> ingress_port : 32 ( .FieldMods ) ;  ( egress_spec : 32 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> <header> <name> data_t </name> <opts> "$fixed_width" |-> 40 </opts> <fields> f1 : 32 ( .FieldMods ) ;  ( b1 : 8 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> </headers> <fieldLists> <fieldList> <name> sel_fields </name> <fields> ( data . f1 ) ;  .FieldListEntryItems </fields> </fieldList> </fieldLists> <fieldListCalcs> <fieldListCalc> <name> sel_hash </name> <fLists> ListItem ( sel_fields ) </fLists> <algorithm> crc16 </algorithm> <outWidth> 14 </outWidth> <fListIndex> 0 </fListIndex> </fieldListCalc> </fieldListCalcs> <calcFields> .CalcFieldCellBag </calcFields> <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 |-> @undef </fieldVals> </instance> <instance> <valid> true </valid> <metadata> false </metadata> <typeName> data_t </typeName> <name> data </name> <fieldVals> b1 |-> @val ( 0 , 8 , false ) f1 |-> @val ( 1 , 32 , false ) </fieldVals> </instance> </instances> <parserStates> <state> <name> start </name> <body> ( extract ( data ) ; .ExtractOrSetStatements ) return ingress ; </body> </state> </parserStates> <statefuls> .StatefulCellBag </statefuls> <tableDirects> .Map </tableDirects> <actions> <action> <name> setf1 </name> <params> val , .ParamList </params> <body> modify_field ( ( data . f1 ) , ( val , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> noop </name> <params> .ParamList </params> <body> .ActionStatements </body> </action> </actions> <actionProfiles> <actionProfile> <name> sel_profile </name> <acts> actions { noop ;  ( setf1 ;  .ActionNameItems ) } </acts> <opts> "$size" |-> 16384 "$selector" |-> sel </opts> <entries> 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </entries> </actionProfile> </actionProfiles> <actionSelectors> <actionSelector> <name> sel </name> <key> sel_hash </key> </actionSelector> </actionSelectors> <tables> <table> <name> test1 </name> <reads> ( data . b1 ) : exact ;  .FieldMatchs </reads> <acts> action_profile : sel_profile ; </acts> <opts> size : 1024 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( 0 , $ctr ( ListItem ( @val ( 0 , 0 , false ) ) ) , @apref ( 0 ) ) ) </rules> </table> </tables> <controlFlows> <control> <name> ingress </name> <body> apply ( test1 ) { .HitMissCases }  .ControlStatements </body> </control> </controlFlows> <cfset> SetItem ( ingress ) </cfset> <calcFieldSet> .Set </calcFieldSet> <ctx> <frameStack> .List </frameStack> <crntTable> test1 </crntTable> <crntRule> 0 </crntRule> </ctx> <packet> ListItem ( @val ( 1 , 32 , false ) ) ListItem ( @val ( 0 , 8 , false ) ) </packet> <packetout> .List </packetout> <parser> <graph> <marked> SetItem ( data ) </marked> <dporder> ListItem ( data ) </dporder> </graph> <index> 2 </index> <lastExt> data </lastExt> <varWidth> . </varWidth> <packetSize> @val ( 5 , 0 , false ) </packetSize> </parser> <buffer> <in> .List </in> <out> .List </out> </buffer> </T>

note the 

<actionProfile> <name> sel_profile </name> <acts> actions { noop ;  ( setf1 ;  .ActionNameItems ) } </acts> <opts> "$size" |-> 16384 "$selector" |-> sel </opts> <entries> 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </entries> </actionProfile> </actionProfiles>

part and specially 

<entries> 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </entries>

Now I have the following rule

rule <k> @val(I:Int,_,false) ~> @deref(P:ActionProfileName , Id:Int) => G[0] ... </k>
     <actionProfiles> <actionProfile> <name> P </name> <entries> (Id |-> G:List) _:Map </entries> <opts> "$selector" |-> S:SelectorName _:Map </opts> ... </actionProfile> ... </actionProfiles>
     <actionSelectors> <actionSelector> <name> S </name> <key> FLC:FieldListCalculationName </key> ... </actionSelector> ... </actionSelectors>

The result of that is: 

<T> <k> ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ~> @setCrntRule ( . ) ~> @setCrntTable ( . ) ~> .HitMissCases ~> .ControlStatements ~> @egress ~> @txenPacket ~> @nextPacket </k> <headers> <header> <name> %standard_metadata_t </name> <opts> .Map </opts> <fields> ingress_port : 32 ( .FieldMods ) ;  ( egress_spec : 32 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> <header> <name> data_t </name> <opts> "$fixed_width" |-> 40 </opts> <fields> f1 : 32 ( .FieldMods ) ;  ( b1 : 8 ( .FieldMods ) ;  .FieldDecs ) </fields> </header> </headers> <fieldLists> <fieldList> <name> sel_fields </name> <fields> ( data . f1 ) ;  .FieldListEntryItems </fields> </fieldList> </fieldLists> <fieldListCalcs> <fieldListCalc> <name> sel_hash </name> <fLists> ListItem ( sel_fields ) </fLists> <algorithm> crc16 </algorithm> <outWidth> 14 </outWidth> <fListIndex> 0 </fListIndex> </fieldListCalc> </fieldListCalcs> <calcFields> .CalcFieldCellBag </calcFields> <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 |-> @undef </fieldVals> </instance> <instance> <valid> true </valid> <metadata> false </metadata> <typeName> data_t </typeName> <name> data </name> <fieldVals> b1 |-> @val ( 0 , 8 , false ) f1 |-> @val ( 1 , 32 , false ) </fieldVals> </instance> </instances> <parserStates> <state> <name> start </name> <body> ( extract ( data ) ; .ExtractOrSetStatements ) return ingress ; </body> </state> </parserStates> <statefuls> .StatefulCellBag </statefuls> <tableDirects> .Map </tableDirects> <actions> <action> <name> setf1 </name> <params> val , .ParamList </params> <body> modify_field ( ( data . f1 ) , ( val , .Args ) ) ;  .ActionStatements </body> </action> <action> <name> noop </name> <params> .ParamList </params> <body> .ActionStatements </body> </action> </actions> <actionProfiles> <actionProfile> <name> sel_profile </name> <acts> actions { noop ;  ( setf1 ;  .ActionNameItems ) } </acts> <opts> "$size" |-> 16384 "$selector" |-> sel </opts> <entries> 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) </entries> </actionProfile> </actionProfiles> <actionSelectors> <actionSelector> <name> sel </name> <key> sel_hash </key> </actionSelector> </actionSelectors> <tables> <table> <name> test1 </name> <reads> ( data . b1 ) : exact ;  .FieldMatchs </reads> <acts> action_profile : sel_profile ; </acts> <opts> size : 1024 ;  .TableOptionals </opts> <rules> ListItem ( $rule ( 0 , $ctr ( ListItem ( @val ( 0 , 0 , false ) ) ) , @apref ( 0 ) ) ) </rules> </table> </tables> <controlFlows> <control> <name> ingress </name> <body> apply ( test1 ) { .HitMissCases }  .ControlStatements </body> </control> </controlFlows> <cfset> SetItem ( ingress ) </cfset> <calcFieldSet> .Set </calcFieldSet> <ctx> <frameStack> .List </frameStack> <crntTable> test1 </crntTable> <crntRule> 0 </crntRule> </ctx> <packet> ListItem ( @val ( 1 , 32 , false ) ) ListItem ( @val ( 0 , 8 , false ) ) </packet> <packetout> .List </packetout> <parser> <graph> <marked> SetItem ( data ) </marked> <dporder> ListItem ( data ) </dporder> </graph> <index> 2 </index> <lastExt> data </lastExt> <varWidth> . </varWidth> <packetSize> @val ( 5 , 0 , false ) </packetSize> </parser> <buffer> <in> .List </in> <out> .List </out> </buffer> </T>

Suggesting that G[0] has been evaluated into ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) rather than @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) )

ehildenb commented 6 years ago

Minimal example please?

Everett H.

On Thu, Sep 14, 2017 at 11:55:21PM +0000, Ali Kheradmand wrote:

Hi I have the following configuration

@val ( 0 , 14 , false ) ~> @deref ( sel_profile , 0 ) ~> @setCrntRule ( . ) ~> @setCrntTable ( . ) ~> .HitMissCases ~> .ControlStatements ~> @egress ~> @txenPacket ~> @nextPacket
%standard_metadata_t .Map ingress_port : 32 ( .FieldMods ) ; ( egress_spec : 32 ( .FieldMods ) ; .FieldDecs )
data_t "$fixed_width" |-> 40 f1 : 32 ( .FieldMods ) ; ( b1 : 8 ( .FieldMods ) ; .FieldDecs )
sel_fields ( data . f1 ) ; .FieldListEntryItems sel_hash ListItem ( sel_fields ) crc16 14 0 .CalcFieldCellBag true true adata> %standard_metadata_t standard_metadata ingress_port |-> @val ( 1 , 32 , false ) egress_spec |-> @undef true false data_t data b1 |-> @val ( 0 , 8 , false ) f1 |-> @val ( 1 , 32 , false ) start ( extract ( data ) ; .ExtractOrSetStatements ) return ingress ; .StatefulCellBag .Map setf1 val , .ParamList modify_field ( ( data . f1 ) , ( val , .Args ) ) ; .ActionStatements noop .ParamList .ActionStatements sel_profile actions { noop ; ( setf1 ; .ActionNa> meItems ) } "$size" |-> 16384 "$selector" |-> sel 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) sel sel_hash test1 ( data . b1 ) : exact ; .FieldMatchs action_profile : sel_profile ; size : 1024 ; .TableOptionals ListItem ( $rule ( 0 , $ctr ( ListItem ( @val ( 0 , 0 , false ) ) ) , @apref ( 0 ) ) )
ingress apply ( test1 ) { .HitMissCases } .ControlStatements SetItem ( ingress ) .Set .List test1 0> ListItem ( @val ( 1 , 32 , false ) ) ListItem ( @val ( 0 , 8 , false ) ) .List SetItem ( data ) ListItem ( data ) 2 data . @val ( 5 , 0 , false ) .List .List

note the

sel_profile actions { noop ; ( setf1 ; .ActionNameItems ) } "$size" |-> 16384 "$selector" |-> sel 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) part and specially 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) Now I have the following rule rule @val(I:Int,_,false) ~> @deref(P:ActionProfileName , Id:Int) => G[0] ... P (Id |-> G:List) _:Map "$selector" |-> S:SelectorName _:Map ... ... S FLC:FieldListCalculationName ... ... The result of that is: ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ~> @setCrntRule ( . ) ~> @setCrntTable ( . ) ~> .HitMissCases ~> .ControlStatements ~> @egress ~> @txenPacket ~> @nextPacket
%standard_metadata_t .Map ingress_port : 32 ( .FieldMods ) ; ( egress_spec : 32 ( .FieldMods ) ; .FieldDecs )
data_t "$fixed_width" |-> 40 f1 : 32 ( .FieldMods ) ; ( b1 : 8 ( .FieldMods ) ; .FieldDecs )
sel_fields ( data . f1 ) ; .FieldListEntryItems sel_hash ListItem ( sel_fields ) crc16 14 0 .CalcFieldCellBag true valid> true %standard_metadata_t standard_metadata ingress_port |-> @val ( 1 , 32 , false ) egress_spec |-> @undef true false data_t data b1 |-> @val ( 0 , 8 , false ) f1 |-> @val ( 1 , 32 , false ) start ( extract ( data ) ; .ExtractOrSetStatements ) return ingress ; .StatefulCellBag .Map setf1 val , .ParamList modify_field ( ( data . f1 ) , ( val , .Args ) ) ; .ActionStatements noop .ParamList .ActionStatements sel_profile actions { > noop ; ( setf1 ; .ActionNameItems ) } "$size" |-> 16384 "$selector" |-> sel 0 |-> ( ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 10 , 0 , false ) ) ) ) ) ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) ) sel sel_hash test1 ( data . b1 ) : exact ; .FieldMatchs action_profile : sel_profile ; size : 1024 ; .TableOptionals ListItem ( $rule ( 0 , $ctr ( ListItem ( @val ( 0 , 0 , false ) ) ) , @apref ( 0 ) ) )
ingress apply ( test1 ) { .HitMissCases } .ControlStatements SetItem ( ingress ) .Set .List tes> t1 0 ListItem ( @val ( 1 , 32 , false ) ) ListItem ( @val ( 0 , 8 , false ) ) .List SetItem ( data ) ListItem ( data ) 2 data . @val ( 5 , 0 , false ) .List .List Suggesting that G[0] has been evaluated into ListItem ( @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) ) rather than @call ( setf1 , $resolved ( ListItem ( @val ( 20 , 0 , false ) ) ) ) — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.*
kheradmand commented 6 years ago

I will try to craft a minimal example. The problem is that the issue does not manifest in small examples that I tried so far.