Commit 7a264fb4 authored by Fabian Kosmale's avatar Fabian Kosmale
Browse files

WIP

parent 87024984
......@@ -165,14 +165,18 @@ class M3ServerProtocoll(WebSocketServerProtocol):
return reply
async def _onGetAllExecutions(self, decoded_message):
loop = asyncio.get_event_loop()
allReads = await loop.run_in_executor(
M3ServerProtocoll.executor,
self.compiler.list_executions,
)
return {
"type": "allReads",
"allReads": allReads
# loop = asyncio.get_event_loop()
# allReads = await loop.run_in_executor(
# M3ServerProtocoll.executor,
# self.compiler.list_executions,
# )
for execution in self.compiler.list_executions():
yield {
"type": "newRead",
"read": execution,
}
yield {
"type": "allReadsFinished",
}
@_ack_nack_helper
......@@ -239,7 +243,8 @@ class M3ServerProtocoll(WebSocketServerProtocol):
self.compiler = await self.outstanding_work
self.outstanding_work = None
try:
reply = await self.handle[decoded_message["type"]](decoded_message)
message_type = decoded_message["type"]
reply = await self.handle[message_type](decoded_message)
except KeyError:
reply = {
"type": "error",
......
......@@ -719,7 +719,6 @@ class Z3Compiler:
return "Cannot decide given program. WTH did you do?"
assert is_sat != z3.unsat, "Program without constraints should always be sat or unknown"
counter = 0
reply = []
self._push()
while is_sat == z3.sat and counter < 50:
logging.info(f"{counter}")
......@@ -736,17 +735,17 @@ class Z3Compiler:
"read_value": read_value,
"read_var": str(var),
})
reply.append({
yield {
"counter": counter,
"reads": execution,
"ordering": self._extract_predecessors_from_model(model),
"reachable": self._extract_reachable_from_model(model),
"writeSeen": self._extract_write_seen_from_model(model),
})
}
is_sat = self._find_new_model(model, counter)
self._pop()
if counter == 50:
print("too many reads!?!")
return reply
def _replay_manually_added_assertions(self) -> Tuple[bool, int]:
logging.info("replaying assertions")
......
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