Unparse InternalBytes using 8-bit encoding

* Unparse InternalBytes using 8-bit encoding

* Format with stylish-haskell

* test: make golden

* Add Strict pragmas

Co-authored-by: ttuegel <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: ttuegel

kore/src/Kore/Internal/InternalBytes.hs

@@ -3,6 +3,8 @@ Copyright   : (c) Runtime Verification, 2019
 License     : NCSA
 -}
 
+{-# LANGUAGE Strict #-}
+
 module Kore.Internal.InternalBytes
     ( InternalBytes (..)
     ) where
@@ -40,14 +42,14 @@ instance Unparse InternalBytes where
     unparse internalBytes@(InternalBytes _ _) =
         "\\dv"
         <> parameters [internalBytesSort]
-        <> arguments [StringLiteral (Encoding.toBase16 internalBytesValue)]
+        <> arguments [StringLiteral (Encoding.decode8Bit internalBytesValue)]
       where
         InternalBytes { internalBytesSort, internalBytesValue } = internalBytes
 
     unparse2 internalBytes@(InternalBytes _ _) =
         "\\dv2"
         <> parameters2 [internalBytesSort]
-        <> arguments2 [StringLiteral (Encoding.toBase16 internalBytesValue)]
+        <> arguments2 [StringLiteral (Encoding.decode8Bit internalBytesValue)]
       where
         InternalBytes { internalBytesSort, internalBytesValue } = internalBytes
 

kore/test/Test/Kore/Builtin/InternalBytes.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE Strict #-}
+
 module Test.Kore.Builtin.InternalBytes
     ( test_update
     , test_get
@@ -14,6 +16,7 @@ module Test.Kore.Builtin.InternalBytes
     , test_int2bytes
     , test_bytes2int
     , test_InternalBytes
+    , test_unparse
     ) where
 
 import Prelude.Kore
@@ -43,6 +46,7 @@ import qualified Kore.Builtin.Encoding as E
 import qualified Kore.Builtin.InternalBytes as InternalBytes
 import Kore.Internal.Pattern
 import Kore.Internal.TermLike
+import Kore.Unparser
 import qualified Pretty
 
 import Test.Kore.Builtin.Builtin
@@ -614,6 +618,15 @@ test_InternalBytes =
         assertEqual "" expect actual
     ]
 
+test_unparse :: [TestTree]
+test_unparse =
+    [ testCase "unparse using 8-bit encoding" $ do
+        let input = asInternal "\x00"
+            actual = (show . unparse) input
+            expect = "/* Fl Fn D Sfa Cl */ \\dv{Bytes{}}(\"\\x00\")"
+        assertEqual "" expect actual
+    ]
+
 -- * Helpers
 
 asInternal :: ByteString -> TermLike VariableName

test/regression-evm-semantics-39dd1e5/test-branching-invalid.sh.out.golden

@@ -96,7 +96,7 @@
                                                         Lbl'-LT-'program'-GT-'{}(
                                                             /* Fl Fn D Sfa Cl */
                                                             \dv{SortBytes{}}(
-                                                                "6003600401600814600c57fe5b00"
+                                                                "`\x03`\x04\x01`\x08\x14`\x0cW\xfe[\x00"
                                                             )
                                                         ),
                                                         /* Fl Fn D Sfa Cl */

test/regression-evm-semantics-39dd1e5/test-straight-line.sh.out.golden

@@ -96,7 +96,7 @@
                                                         Lbl'-LT-'program'-GT-'{}(
                                                             /* Fl Fn D Sfa Cl */
                                                             \dv{SortBytes{}}(
-                                                                "7f00000000000000000000000000000000000000000000000000000000000000037f000000000000000000000000000000000000000000000000000000000000000401fe"
+                                                                "\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x03\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x04\x01\xfe"
                                                             )
                                                         ),
                                                         /* Fl Fn D Sfa Cl */