Use 8-bit encoding of Bytes (#2257)

Author: ttuegel

kore/src/Kore/Builtin/Encoding.hs

@@ -6,6 +6,7 @@ License     : NCSA
 module Kore.Builtin.Encoding
     ( encode8Bit
     , decode8Bit
+    , parse8Bit
     , parseBase16
     , toBase16
     ) where
@@ -33,6 +34,7 @@ import Data.Word
     )
 import Text.Megaparsec
     ( Parsec
+    , (<?>)
     )
 import qualified Text.Megaparsec as Parsec
 
@@ -62,6 +64,23 @@ encode8Bit =
                 , show int
                 ]
 
+{- | Encode text using an 8-bit encoding.
+
+Each 'Char' in the text is interpreted as a 'Data.Word.Word8'. It is an error if
+any character falls outside that representable range.
+
+ -}
+parse8Bit :: Parsec Void Text ByteString
+parse8Bit =
+    ByteString.pack <$> many parseByte
+  where
+    parseByte :: Parsec Void Text Word8
+    parseByte =
+        fromIntegral . Char.ord <$> Parsec.satisfy is8Bit <?> "8-bit value"
+
+    is8Bit :: Char -> Bool
+    is8Bit c = c < '\x100'
+
 decode8Bit :: ByteString -> Text
 decode8Bit =
     ByteString.unpack

kore/src/Kore/Builtin/InternalBytes.hs

@@ -149,7 +149,7 @@ patternVerifierHook =
     patternVerifierWorker external =
         case externalChild of
             StringLiteral_ literal -> do
-                bytesValue <- Builtin.parseString Encoding.parseBase16 literal
+                bytesValue <- Builtin.parseString Encoding.parse8Bit literal
                 (return . InternalBytesF . Const)
                     InternalBytes { bytesSort, bytesValue }
             _ -> Kore.Error.koreFail "Expected literal string"

kore/src/Kore/Builtin/InternalBytes/InternalBytes.hs

@@ -67,11 +67,13 @@ sort :: Text
 sort = "BYTES.Bytes"
 
 
--- | Render a 'ByteString' as an internal domain value of the given sort.
--- | The result sort should be hooked to the builtin @Bytes@ sort, but this is
--- | not checked.
--- |
--- | See also: 'sort'.
+{- | Render a 'ByteString' as an internal domain value of the given sort.
+
+The result sort should be hooked to the builtin @Bytes@ sort, but this is
+not checked.
+
+See also: 'sort'.
+ -}
 asInternal
     :: InternalVariable variable
     => Sort        -- ^ resulting sort
@@ -80,20 +82,21 @@ asInternal
 asInternal bytesSort bytesValue =
     TermLike.markSimplified $ mkInternalBytes bytesSort bytesValue
 
--- | Render a 'Bytes' as a domain value pattern of the given sort.
--- |
--- | The result sort should be hooked to the builtin @Bytes@ sort, but this is
--- | not checked.
--- |
--- | See also: 'sort'.
+{- | Render a 'Bytes' as a domain value pattern of the given sort.
+
+The result sort should be hooked to the builtin @Bytes@ sort, but this is
+not checked.
+
+See also: 'sort'.
+ -}
 asTermLike
     :: InternalVariable variable
     => InternalBytes  -- ^ builtin value to render
     -> TermLike variable
 asTermLike InternalBytes { bytesSort, bytesValue }  =
     mkDomainValue DomainValue
         { domainValueSort = bytesSort
-        , domainValueChild = mkStringLiteral $ Encoding.toBase16 bytesValue
+        , domainValueChild = mkStringLiteral $ Encoding.decode8Bit bytesValue
         }
 
 internalize

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

@@ -603,6 +603,14 @@ test_InternalBytes =
                 mkDomainValue
                 $ DomainValue bytesSort
                 $ mkStringLiteral "00"
+            expect = Right $ asInternal "00"
+            actual = verifyPattern (Just bytesSort) unverified
+        assertEqual "" expect actual
+    , testCase "\\dv{Bytes{}}(\"\x00\")" $ do
+        let unverified =
+                mkDomainValue
+                $ DomainValue bytesSort
+                $ mkStringLiteral "\x00"
             expect = Right $ asInternal "\x00"
             actual = verifyPattern (Just bytesSort) unverified
         assertEqual "" expect actual

test/regression-c-semantics/.gitignore

@@ -0,0 +1 @@
+definition.kore

test/regression-c-semantics/Makefile

@@ -0,0 +1,6 @@
+include $(CURDIR)/../include.mk
+
+definition.kore: definition.kore.gz
+	zcat $< >$@
+
+test-regression-c-semantics.sh.out: definition.kore executable.kore

test/regression-c-semantics/definition.kore.gz

@@ -0,0 +1,3 @@
+#!/bin/sh
+
+$KORE_PARSER --no-print-definition --no-print-pattern definition.kore --pattern executable.kore --module C