diff --git a/mc_openapi/api.py b/mc_openapi/api.py index f3f003412b2172b5469a4b5bd9b0972714ddc13f..f08700a05527b6107179eec9964971e48fe28b77 100644 --- a/mc_openapi/api.py +++ b/mc_openapi/api.py @@ -42,31 +42,18 @@ def handleDOMLX(doml_xmi: bytes, callback) -> dict: dmc = init_model(doml_xmi, doml_version) - return callback(dmc) + res = callback(dmc) + + return res - except ( - BadDOMLException, - UnsupportedDOMLVersionException, - MissingInfrastructureLayerException, - NoActiveConcreteLayerException - ) as e: - return JSONResponse( - status_code=400, - content=jsonable_encoder({ - "message": e.errors, - "debug_message": traceback.format_exc() - }) - ) except (RuntimeError, Exception) as e: - logging.error(traceback.format_exc()) - return JSONResponse( - status_code=400, - content=jsonable_encoder({ - "message": "An error has occurred. It could be an error within your DOML file. If it persist, try specifying DOML version manually.", - "debug_message": traceback.format_exc() - }) - ) - + ERR_MSG = "An error has occurred.\nIt could be an error within your DOML file.\nIf it persist, try specifying DOML version manually." + logging.exception(e) + return { + "type": "error", + "message": e.message or ERR_MSG, + "debug_message": traceback.format_exc() + } @app.post("/modelcheck") async def mc(request: Request): @@ -81,11 +68,20 @@ async def csp(request: Request): @app.post("/modelcheck_html") async def mc_html(request: Request): doml_xmi = await request.body() - res = handleDOMLX(doml_xmi, verify_model) - return templates.TemplateResponse("mc.html", {"request": request, **res}) + res = handleDOMLX(doml_xmi, verify_model) + print(res) + if res.get("type") == "error": + return templates.TemplateResponse("error.html", {"request": request, **res}) + else: + return templates.TemplateResponse("mc.html", {"request": request, **res}) + @app.post("/csp_html") async def csp_html(request: Request): doml_xmi = await request.body() - res = handleDOMLX(doml_xmi, verify_csp_compatibility) - return templates.TemplateResponse("csp.html", {"request": request, **res}) + res = handleDOMLX(doml_xmi, verify_csp_compatibility) + if res.get("type") == "error": + return templates.TemplateResponse("error.html", {"request": request, **res}) + else: + return templates.TemplateResponse("csp.html", {"request": request, **res}) + \ No newline at end of file diff --git a/mc_openapi/assets/templates/error.html b/mc_openapi/assets/templates/error.html new file mode 100644 index 0000000000000000000000000000000000000000..3afeee1fafcdc4d6ff55489731fd6be11494e190 --- /dev/null +++ b/mc_openapi/assets/templates/error.html @@ -0,0 +1,24 @@ +{% extends "base.html" %} + +{% block content %} + +<h1 class="title">Error</h1> +<div class="message is-danger"> + <div class="message-header"> + <p> + An error occurred while validating the DOML + </p> + </div> + <div class="message-body"> + <h2 class="title is-6 my-2">Description</h2> + <p>{{message}}</p> + <details> + <summary class="title is-6 my-2">Debug Message</summary> + <pre class="is-family-monospace message-body"> + {{debug_message}} + </pre> + </details> + </div> +</div> + +{% endblock content %} \ No newline at end of file diff --git a/mc_openapi/doml_mc/domlr_parser/exceptions.py b/mc_openapi/doml_mc/domlr_parser/exceptions.py index 630ce72e3c0ec7285c42d5bbc255b1d65fd42d26..44ba418127398291a5449923bc729fe06596be0d 100644 --- a/mc_openapi/doml_mc/domlr_parser/exceptions.py +++ b/mc_openapi/doml_mc/domlr_parser/exceptions.py @@ -18,3 +18,8 @@ class RequirementBadSyntaxException(RequirementException): def __init__(self, line: int, col: int, message: str, *args: object) -> None: super().__init__(*args) self.message = f"Syntax Error at Ln {line}, Col {col}:\n{message}" + +class ParserException(Exception): + def __init__(self, *args: object) -> None: + super().__init__(*args) + self.errors = "Failed to parse DOMLR." \ No newline at end of file diff --git a/mc_openapi/doml_mc/domlr_parser/parser.py b/mc_openapi/doml_mc/domlr_parser/parser.py index 2a2ab5e6db3e9d6535238fd8beb5302b96870f20..00fdc260421d328c5149200e8865e1cb4f839fa2 100644 --- a/mc_openapi/doml_mc/domlr_parser/parser.py +++ b/mc_openapi/doml_mc/domlr_parser/parser.py @@ -5,8 +5,7 @@ from doml_synthesis import State from lark import Lark, UnexpectedCharacters, UnexpectedEOF from z3 import Not -from mc_openapi.doml_mc.domlr_parser.exceptions import \ - RequirementBadSyntaxException +from mc_openapi.doml_mc.domlr_parser.exceptions import ParserException, RequirementBadSyntaxException, RequirementMissingKeyException from mc_openapi.doml_mc.domlr_parser.utils import StringValuesCache, VarStore from mc_openapi.doml_mc.imc import RequirementStore @@ -73,6 +72,7 @@ class Parser: msg = _get_error_desc_for_unexpected_characters(e, input) raise RequirementBadSyntaxException(e.line, e.column, msg) + def _get_error_desc_for_unexpected_characters(e: UnexpectedCharacters, input: str): # Error description msg = "Syntax Error:\n\n" diff --git a/mc_openapi/doml_mc/exceptions.py b/mc_openapi/doml_mc/exceptions.py index 1a36fef4232906d76590cb4fc6f9e3954517d906..a94ab25111da89185f6c5eecca42906c255af76d 100644 --- a/mc_openapi/doml_mc/exceptions.py +++ b/mc_openapi/doml_mc/exceptions.py @@ -4,20 +4,20 @@ from mc_openapi.doml_mc.intermediate_model.metamodel import DOMLVersion class BadDOMLException(Exception): def __init__(self, message: str = None, *args: object) -> None: super().__init__(*args) - self.errors = message or "The submitted DOML contains some kind of error." + self.message = message or "The submitted DOML contains some kind of error." class UnsupportedDOMLVersionException(Exception): def __init__(self, message: str = None, *args: object) -> None: super().__init__(*args) - self.errors = message or "The DOML version is not supported." + self.message = message or "The DOML version is not supported." class MissingInfrastructureLayerException(Exception): def __init__(self, message: str = None, *args: object) -> None: super().__init__(*args) - self.errors = message or "Abstract infrastructure layer is missing from DOML." + self.message = message or "Abstract infrastructure layer is missing from DOML." class NoActiveConcreteLayerException(Exception): def __init__(self, message: str = None, *args: object) -> None: super().__init__(*args) - self.errors = message or "No active concrete infrastructure layer has been specified in DOML." + self.message = message or "No active concrete infrastructure layer has been specified in DOML." diff --git a/mc_openapi/doml_mc/main.py b/mc_openapi/doml_mc/main.py index 48af629fb93c5dbcc584cf254b4e65cfac5e2cd6..c4befd1988e35951ce627ba41631a7b084b70d24 100644 --- a/mc_openapi/doml_mc/main.py +++ b/mc_openapi/doml_mc/main.py @@ -83,13 +83,14 @@ def verify_model( req_store, threads=threads, user_str_values=user_req_str_consts, - disable_multithreading=(threads == 1) + disable_multithreading=True #(threads == 1) ) res = results.summarize() res['doml_version'] = dmc.doml_version.name res['result'] = res['result'].name + res['type'] = 'message' # logging.info(res) @@ -159,5 +160,7 @@ def synthesize_model(dmc: ModelChecker, external_domlr: str, max_tries: int): def verify_csp_compatibility(dmc: ModelChecker): - return CSPCompatibility.check(dmc.intermediate_model, dmc.doml_version) + res = CSPCompatibility.check(dmc.intermediate_model, dmc.doml_version) + res['type'] = 'message' + return res \ No newline at end of file