Commit 51e47dc8 authored by Fabian Kosmale's avatar Fabian Kosmale
Browse files

Converted Instruction from uninterpreted sort to enum

This should allow for a better mapping between instructions and
statements.
parent 347f685b
......@@ -573,8 +573,7 @@ class PrintlnStatement(Statement):
self.expressions = tokens
def __repr__(self):
return 'println({});'.format(", ".join(repr(tok) for tok in
self.expressions))
return 'println({});'.format(", ".join(repr(tok) for tok in self.expressions))
def get_cfg_exit_nodes(self): # pylint: disable=useless-super-delegation
return super().get_cfg_exit_nodes()
......@@ -660,6 +659,7 @@ class VariableDeclaration(Statement):
if isinstance(self.initial_value, VariableUsage):
# do not attempt to simplfy expression when it already is a simple
# read of a global
replacement_counter.global_operations += 1
return [self]
reads, replacements = self.initial_value.extract_global_read(tt, replacement_counter)
self.initial_value.replace_globals(replacements)
......
This diff is collapsed.
......@@ -4,7 +4,7 @@ import asyncio
import websockets
from pseuco_parser import createParser, UnsupportedPseuCoException
from semantic import Z3Compiler, seqconsist_axioms, weak_order_axioms
from semantic import Z3Compiler, MemoryModel
def parseProgram(program):
......@@ -42,9 +42,9 @@ async def parse(websocket, path):
elif decoded_message["type"] == "listAllReads":
reply = {"type": "allReads"}
if decoded_message["memoryModel"] == "seqConsist":
reply["allReads"] = compiler.check_sat(seqconsist_axioms)
reply["allReads"] = compiler.check_sat(MemoryModel.SequentialConsistency)
elif decoded_message["memoryModel"] == "weak":
reply["allReads"] = compiler.check_sat(weak_order_axioms)
reply["allReads"] = compiler.check_sat(MemoryModel.WeakConsistency)
except UnsupportedPseuCoException as e:
reply = {
"type": "error",
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment