Skip to content

Add simplifications to #cast Transmute [u8; 8] -> u64 #816

@dkcumming

Description

@dkcumming

#804 introduces a rule to remove a thunk for transmute casts between [u8; 8] -> u64. However these large expressions can be simplified into ?AMOUNT:Int as they are entirely symbolic. This can be seen in test_process_close_account See details below.

The solution is likely to directly use Bytes2Int simplification rule from the p-token.md file:

// Amount Round-trip Simplifications:
rule Bytes2Int(
#bytesFrom(
ListItem(Integer(AMOUNT &Int 255, 8, false))
ListItem(Integer(AMOUNT >>Int 8 &Int 255, 8, false))
ListItem(Integer(AMOUNT >>Int 8 >>Int 8 &Int 255, 8, false))
ListItem(Integer(AMOUNT >>Int 8 >>Int 8 >>Int 8 &Int 255, 8, false))
ListItem(Integer(AMOUNT >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255, 8, false))
ListItem(Integer(AMOUNT >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255, 8, false))
ListItem(Integer(AMOUNT >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255, 8, false))
ListItem(Integer(AMOUNT >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255, 8, false))
) ,
LE,
Unsigned
) => AMOUNT
[simplification, symbolic(AMOUNT), preserves-definedness]

(1 step)
443
   <generatedTop>
     <kmir>
       <k>
         #cast ( Range ( ListItem (Integer ( ?AMOUNT:Int &Int 255 , 8 , false ))
          ListItem (Integer ( ?AMOUNT:Int >>Int 8 &Int 255 , 8 , false ))
          ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 &Int 255 , 8 , false ))
          ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
          ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
          ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
          ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
          ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
          ) , castKindTransmute , ty ( 600721 ) , ty ( 600142 ) )

Does not thunk but creates a the expression:

(1 step)
444
   <generatedTop>
     <kmir>
       <k>
         Integer ( ?AMOUNT:Int &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 &Int 18446744073709551615 , 64 , false )

Which then is stored in the locals without simplification:

<locals>
  ListItem (typedValue ( Integer ( ?AMOUNT:Int &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 &Int 18446744073709551615 , 64 , false ) , ty ( 600142 ) , mutabilityMut ))

But we want is:

ListItem (typedValue ( Integer ( ?AMOUNT:Int, 64 , false ) , ty ( 600142 ) , mutabilityMut ))

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions