Skip to content
Snippets Groups Projects
Unverified Commit db2ed000 authored by Andrea Franchini's avatar Andrea Franchini
Browse files

Add better parser error description

parent e025ecdf
No related branches found
No related tags found
No related merge requests found
......@@ -3,6 +3,7 @@ import argparse
from mc_openapi.app_config import app
from mc_openapi.doml_mc import DOMLVersion
from mc_openapi.doml_mc.dsl_parser.exceptions import RequirementException
from mc_openapi.doml_mc.mc import ModelChecker
from mc_openapi.doml_mc.mc_result import MCResult
......@@ -45,7 +46,7 @@ else:
# Read the user requirements written in DSL
user_reqs = reqsf.read()
try:
# Check satisfiability
results = dmc.check_requirements(
threads=args.threads,
......@@ -61,4 +62,5 @@ else:
else:
print(res.name)
print("\033[91m{}\033[00m".format(msg))
\ No newline at end of file
except RequirementException as e:
print(e.message)
\ No newline at end of file
class RequirementException(Exception):
message: str
def __repr__(self) -> str:
return self.message
class RequirementMissingKeyException(RequirementException):
def __init__(self, key_type: str, key: str, close_matches: list[str], *args: object) -> None:
super().__init__(*args)
fix_syntax = lambda x: x.replace("_", ".").replace("::", "->")
key = fix_syntax(key)
close_matches = list(map(fix_syntax, close_matches))
self.message = f"Error: no {key_type} found named '{key}'.\n"
if close_matches:
self.message += "Perhaps you meant...\n"
self.message += "".join([f"- '{match}'\n" for match in close_matches])
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}"
TOKENS:
FLIP_EXPR: |
a declaration of a requirement.
To declare a requirement use:
• '+' to declare a requirement
• '-' to declare a requirement in negation form, which means
that if it's satisfied, then the DOML does not respect the
requirements.
ESCAPED_STRING: a string. Strings are enclosed by double quotes '"'.
BOOL: a boolean value. It can be 'true' or 'false'.
NUMBER: a number. It must be an integer.
VALUE: a value constant. Values must start with an uppercase letter.
CONST: a logic variable. Variables must start with a lowercase letter.
IS: |
a statement such as:
• 'is', 'is not' followed by a class or a variable
• 'has attribute' followed by an attribute name and a value
• 'has association' followed by an association name and a variable.
NOT: a 'not' before an expression or a quantifier.
OR: a logical connective such as 'or' between expressions.
AND: a logical connective such as 'and' between expressions.
IFF: a logical connective such as 'iff' between expressions.
IMPLIES: a logical connective such as 'implies' between expressions.
COMMA: a ',' separating bounded variables after an 'exists'/'forall'
LPAR: a '(' after which an expression begins.
RPAR: a ')' closing a previous '('.
RELATIONSHIP: |
a valid relationship name.
Relationships consists of 'package.class->relationship', with no spaces around '.' and '->'.
EXISTS: a 'exists' quantifier.
FORALL: a 'forall' quantifier.
CLASS_PREFIX: a 'class' followed by a class name
ERR_DESC_SYMBOL: a '---' (three hyphens) to separate the logic expression from the error message.
HINTS:
DOT: If you're trying to use a class, did you put 'class' before the class name?
\ No newline at end of file
requirements : requirement (requirement)*
requirement : FLIP_EXPR req_name expression "---" error_desc
requirement : FLIP_EXPR req_name expression ERR_DESC_SYMBOL error_desc
req_name : ESCAPED_STRING
error_desc : ESCAPED_STRING
......@@ -59,6 +59,8 @@ CONST: (LCASE_LETTER) ("_"|LETTER|DIGIT)*
// Value must start with uppercase letter
VALUE: (UCASE_LETTER) ("_"|LETTER|DIGIT)*
ERR_DESC_SYMBOL: "---"
// Comment: python/sh style
COMMENT: /#[^\n]*/
......
......@@ -2,7 +2,9 @@ import os
import re
from typing import Callable
from lark import Lark, Transformer
import yaml
from lark import Lark, Transformer, UnexpectedCharacters
from mc_openapi.doml_mc.dsl_parser.exceptions import RequirementBadSyntaxException
from mc_openapi.doml_mc.dsl_parser.utils import (RefHandler, StringValuesCache,
VarStore)
from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
......@@ -15,14 +17,20 @@ from z3 import And, Exists, ExprRef, ForAll, Implies, Not, Or, Solver, Xor
class ParserData:
def __init__(self) -> None:
grammar_path = os.path.join(os.path.dirname(__file__), "grammar.lark")
exceptions_path = os.path.join(os.path.dirname(__file__), "exceptions.yaml")
with open(grammar_path, "r") as grammar:
self.grammar = grammar.read()
with open(exceptions_path, "r") as exceptions:
self.exceptions = yaml.safe_load(exceptions)
PARSER_DATA = ParserData()
class Parser:
def __init__(self, grammar: str = ParserData().grammar):
def __init__(self, grammar: str = PARSER_DATA.grammar):
self.parser = Lark(grammar, start="requirements")
def parse(self, input: str):
try:
self.tree = self.parser.parse(input)
const_store = VarStore()
......@@ -31,6 +39,9 @@ class Parser:
transformer = DSLTransformer(const_store, user_values_cache)
return RequirementStore(transformer.transform(self.tree)), user_values_cache.get_list()
except UnexpectedCharacters as e:
msg = _get_error_desc_for_unexpected_characters()
raise RequirementBadSyntaxException(e.line, e.column, msg)
class DSLTransformer(Transformer):
# These callbacks will be called when a rule with the same name
......@@ -55,7 +66,7 @@ class DSLTransformer(Transformer):
flip_expr: bool = args[0].value == "-"
name: str = args[1]
expr: Callable[[SMTEncoding, SMTSorts], ExprRef] = args[2]
errd: Callable[[Solver, SMTSorts, IntermediateModel, int], str] = args[3]
errd: Callable[[Solver, SMTSorts, IntermediateModel, int], str] = args[4]
index = self.const_store.get_index_and_push()
return Requirement(
expr,
......@@ -196,3 +207,21 @@ class DSLTransformer(Transformer):
return msg + ("\n\n\tNOTES:" + notes if notes else "")
return err_callback
def _get_error_desc_for_unexpected_characters(e: UnexpectedCharacters):
# Error description
desc = ""
desc_prefix = "Expected one of the following:\n"
for val in e.allowed:
val = PARSER_DATA.exceptions["TOKENS"].get(val, "")
desc += (f"{val}\n") if val else ""
# Suggestion that might be useful
hints = ""
if e.char == ".":
hints += PARSER_DATA.exceptions["HINTS"]["DOT"]
# Print line highlighting the error
ctx = e.get_context(input)
msg = ctx
msg += (desc_prefix + desc) if desc else "Unknown error occurred during parsing!"
msg += f"\nHINTS:\n{hints}" if hints else ""
\ No newline at end of file
from difflib import get_close_matches
from mc_openapi.doml_mc.dsl_parser.exceptions import \
RequirementMissingKeyException
from mc_openapi.doml_mc.imc import SMTEncoding, SMTSorts
from z3 import Const, DatatypeRef, ExprRef, FuncDeclRef, SortRef
class StringValuesCache:
def __init__(self) -> None:
self.values: set[str] = set()
......@@ -74,9 +79,8 @@ class RefHandler:
if _class is not None:
return _class
else:
raise Exception(f"No class named '{class_name}' found.")
# TODO: Try to suggest the correct class with difflib
# see: https://docs.python.org/3/library/difflib.html?highlight=get_close_matches#difflib.get_close_matches
close_matches = get_close_matches(class_name, enc.classes.keys())
raise RequirementMissingKeyException("class", class_name, close_matches)
def get_association(enc: SMTEncoding, assoc_name: str) -> DatatypeRef:
assoc_name = assoc_name.replace(".", "_")
......@@ -85,7 +89,8 @@ class RefHandler:
if assoc is not None:
return assoc
else:
raise Exception(f"No association named '{assoc_name}' found.")
close_matches = get_close_matches(assoc_name, enc.associations.keys())
raise RequirementMissingKeyException("association", assoc_name, close_matches)
def get_association_rel(enc: SMTEncoding, a: ExprRef, rel: DatatypeRef, b: ExprRef) -> DatatypeRef:
return enc.association_rel(a, rel, b)
......@@ -97,7 +102,8 @@ class RefHandler:
if attr is not None:
return attr
else:
raise Exception(f"No attribute named '{attr_name}' found.")
close_matches = get_close_matches(attr_name, enc.attributes.keys())
raise RequirementMissingKeyException("attribute", attr_name, close_matches)
def get_attribute_rel(enc: SMTEncoding, a: ExprRef, rel: DatatypeRef, b: ExprRef) -> DatatypeRef:
return enc.attribute_rel(a, rel, b)
......
# vm, iface = get_consts(smtsorts, ["vm", "iface"])
# return And(
# smtenc.element_class_fun(vm) == smtenc.classes["infrastructure_VirtualMachine"],
# Not(
# Exists(
# [iface],
# ENCODINGS.association_rel(vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], iface)
# )
# )
# )
+ "All VMs have at least one interface 1"
vm is class infrastructure.VirtualMachine
and
not exists iface (
vm has association infrastructure.ComputingNode->ifaces iface
and
vm has attribute infrastructure.ComputingNode->ifaces X
)
---
"VM {vm} has no associated interface."
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment