Merge branch 'develop' into dev/cjs/24g05/install-build-deps-script

.github/workflows/update-deps.yml

@@ -59,7 +59,7 @@ jobs:
           cd llvm-backend/src/main/native/llvm-backend
           git checkout "${llvm_backend_version}"
           cd -
-          sed -i 's!      url = "github:runtimeverification/llvm-backend/.*";!      url = "github:runtimeverification/llvm-backend/'"${llvm_backend_version}"'";!' flake.nix
+          sed -i 's!    llvm-backend.url = "github:runtimeverification/llvm-backend/.*";!    llvm-backend.url = "github:runtimeverification/llvm-backend/'"${llvm_backend_version}"'";!' flake.nix
           if git add flake.nix llvm-backend/src/main/native/llvm-backend && git commit -m "flake.nix, llvm-backend/src/main/native/llvm-backend: update to version ${llvm_backend_version}"; then
             changed=true
           fi

deps/haskell-backend_release

@@ -1 +1 @@
-v0.1.40
+v0.1.46

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.57
+0.1.59

flake.nix

@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.56";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.59";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.32";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

pyk/src/pyk/kast/outer_parser.py

@@ -379,10 +379,13 @@ def _maybe_att(self) -> Att:
             value: str
             if self._la.type == TokenType.LPAREN:
                 self._consume()
-                if self._la.type is TokenType.ATTR_CONTENT:
-                    value = self._consume()
-                else:
-                    value = _dequote_string(self._match(TokenType.STRING))
+                match self._la.type:
+                    case TokenType.ATTR_CONTENT:
+                        value = self._consume()
+                    case TokenType.STRING:
+                        value = _dequote_string(self._consume())
+                    case _:
+                        value = ''
                 self._match(TokenType.RPAREN)
             else:
                 value = ''

pyk/src/pyk/kllvm/hints/prooftrace.py

@@ -201,7 +201,7 @@ def name(self) -> str:
 
     @property
     def relative_position(self) -> str:
-        """Return the relative position of the LLVM function event in the proof trace. Ex.: (0:0:0:0)."""
+        """Return the relative position of the LLVM function event in the proof trace."""
         return self._function_event.relative_position
 
     @property
@@ -243,7 +243,7 @@ def name(self) -> str:
 
     @property
     def relative_position(self) -> str:
-        """Return the relative position of the hook event in the proof trace. Ex.: (0:0:0:0)."""
+        """Return the relative position of the hook event in the proof trace."""
         return self._hook_event.relative_position
 
     @property

pyk/src/pyk/kore/rpc.py

@@ -66,9 +66,9 @@ def __init__(self, bug_report_id: str | None = None, bug_report: BugReport | Non
         self._bug_report_id = bug_report_id
         self._bug_report = bug_report
 
-    def request(self, req: str, request_id: int, method_name: str) -> str:
+    def request(self, req: str, request_id: str, method_name: str) -> str:
         base_name = self._bug_report_id if self._bug_report_id is not None else 'kore_rpc'
-        req_name = f'{base_name}/{id(self)}/{request_id:03}'
+        req_name = f'{base_name}/{id(self)}/{request_id}'
         if self._bug_report:
             bug_report_request = f'{req_name}_request.json'
             self._bug_report.add_file_contents(req, Path(bug_report_request))
@@ -340,24 +340,24 @@ def close(self) -> None:
         self._transport.close()
 
     def request(self, method: str, **params: Any) -> dict[str, Any]:
-        old_id = self._req_id
+        req_id = f'{id(self)}-{self._req_id:03}'
         self._req_id += 1
 
         payload = {
             'jsonrpc': self._JSON_RPC_VERSION,
-            'id': old_id,
+            'id': req_id,
             'method': method,
             'params': params,
         }
 
         req = json.dumps(payload)
-        resp = self._transport.request(req, old_id, method)
+        resp = self._transport.request(req, req_id, method)
         if not resp:
             raise RuntimeError('Empty response received')
 
         data = json.loads(resp)
         self._check(data)
-        assert data['id'] == old_id
+        assert data['id'] == req_id
 
         return data['result']
 

pyk/src/tests/unit/kast/test_outer_parser.py

@@ -113,6 +113,26 @@
         'syntax Foo ::= "foo"',
         SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),)),)),)),
     ),
+    (
+        'syntax Foo ::= "foo" [symbol]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', ''),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol()]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', ''),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol("")]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', ''),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol(foo)]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', 'foo'),))),)),)),
+    ),
+    (
+        'syntax Foo ::= "foo" [symbol("foo")]',
+        SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((Terminal('foo'),), att=Att((('symbol', 'foo'),))),)),)),
+    ),
     (
         'syntax Foo ::= Bar',
         SyntaxDefn(SortDecl('Foo'), (PriorityBlock((Production((NonTerminal(Sort('Bar')),)),)),)),