diff --git a/mc_openapi/doml_mc/domlr_parser/grammar.lark b/mc_openapi/doml_mc/domlr_parser/grammar.lark index 5fc30f6b6e1cda02bfea5c3459d527aa398f9124..2cb5539a138b9cd90129a9c9599fc88c030c8aa0 100644 --- a/mc_openapi/doml_mc/domlr_parser/grammar.lark +++ b/mc_openapi/doml_mc/domlr_parser/grammar.lark @@ -23,12 +23,12 @@ error_desc : ESCAPED_STRING | "(" expression ")" | property -?property : CONST "has" RELATIONSHIP (CONST|attr_rhs) -> relationship_expr - | const_or_class "is" const_or_class -> equality - | const_or_class "is not" const_or_class -> inequality +?property : CONST "has" RELATIONSHIP CONST -> rel_elem_expr + | CONST "has" RELATIONSHIP COMPARISON_OP value -> rel_attr_value_expr + | CONST "has" RELATIONSHIP COMPARISON_OP CONST RELATIONSHIP -> rel_attr_elem_expr + | const_or_class "is" const_or_class -> equality + | const_or_class "is not" const_or_class -> inequality -?attr_rhs : COMPARISON_OP value -> attribute_value - | COMPARISON_OP CONST RELATIONSHIP -> rhs_const_attribute bound_consts : [CONST ("," CONST)*] diff --git a/mc_openapi/doml_mc/domlr_parser/parser.py b/mc_openapi/doml_mc/domlr_parser/parser.py index 57f7f89ffb47ecd40382575761ac356fdfb26052..d5d3edbe74546ffc547d1c61b629b2b3b118ddef 100644 --- a/mc_openapi/doml_mc/domlr_parser/parser.py +++ b/mc_openapi/doml_mc/domlr_parser/parser.py @@ -127,38 +127,98 @@ class DOMLRTransformer(Transformer): def forall(self, args): return lambda enc, sorts: ForAll(args[0](enc, sorts), args[1](enc, sorts)) - def relationship_expr(self, args): - print(args) + # def relationship_expr(self, args): + # print(args) + # rel_name = args[1].value + + # def _gen_rel_expr(enc: SMTEncoding, sorts: SMTSorts): + # rel, rel_type = RefHandler.get_relationship(enc, rel_name) + + # if rel_type == RefHandler.ASSOCIATION: + # self.const_store.use(args[0].value) + # self.const_store.use(args[2].value) + + # return RefHandler.get_association_rel( + # enc, + # RefHandler.get_const(args[0].value, sorts), + # rel, + # RefHandler.get_const(args[2].value, sorts) + # ) + # elif rel_type == RefHandler.ATTRIBUTE: + # self.const_store.use(args[0].value) + + # return RefHandler.get_attribute_rel( + # enc, + # RefHandler.get_const(args[0].value, sorts), + # rel, + # args[2](enc, sorts) + # ) + # else: + # raise f"Error parsing relationship {rel_name}" + + # return _gen_rel_expr + + def rel_elem_expr(self, args): + """An ASSOCIATION relationship""" rel_name = args[1].value + self.const_store.use(args[0].value) + self.const_store.use(args[2].value) - def _gen_rel_expr(enc: SMTEncoding, sorts: SMTSorts): + def _gen_rel_elem_expr(enc: SMTEncoding, sorts: SMTSorts): rel, rel_type = RefHandler.get_relationship(enc, rel_name) - - if rel_type == RefHandler.ASSOCIATION: - self.const_store.use(args[0].value) - self.const_store.use(args[2].value) - return RefHandler.get_association_rel( - enc, - RefHandler.get_const(args[0].value, sorts), - rel, - RefHandler.get_const(args[2].value, sorts) - ) - elif rel_type == RefHandler.ATTRIBUTE: - self.const_store.use(args[0].value) + assert rel_type == RefHandler.ASSOCIATION + + return RefHandler.get_association_rel( + enc, + RefHandler.get_const(args[0].value, sorts), + rel, + RefHandler.get_const(args[2].value, sorts) + ) + return _gen_rel_elem_expr - return RefHandler.get_attribute_rel( - enc, - RefHandler.get_const(args[0].value, sorts), + def rel_attr_value_expr(self, args): + """An ATTRIBUTE relationship""" + + rel_name = args[1].value + def _gen_rel_attr_value_expr(enc: SMTEncoding, sorts: SMTSorts): + elem = RefHandler.get_const(args[0].value, sorts) + rel, rel_type = RefHandler.get_relationship(enc, rel_name) + assert rel_type == RefHandler.ATTRIBUTE + + rhs_value, rhs_value_type = args[3] + rhs_value = rhs_value(enc, sorts) + op = args[2].value + + if rhs_value_type == RefHandler.INTEGER: + + lhs_value = RefHandler.get_value("x", sorts) + + return And( + RefHandler.get_attribute_rel(enc, + elem, + rel, + lhs_value + ), + self.compare_int(sorts, op, lhs_value, rhs_value) + ) + elif rhs_value_type == RefHandler.STRING or rhs_value_type == RefHandler.BOOLEAN: + expr = RefHandler.get_attribute_rel(enc, + elem, rel, - args[2](enc, sorts) + rhs_value ) - else: - raise f"Error parsing relationship {rel_name}" - - return _gen_rel_expr + if op == "==": + return expr + elif op == "!=": + return Not(expr) + else: + raise f'Invalid compare operator "{op}". It must be "==" or "!=".' + + + return _gen_rel_attr_value_expr - def attribute_value(self, args): + def rel_attr_elem_expr(self, args): """Parse rhs of expression containing: <, <=, >, >=, ==, != can be followed by a NUMBER ==, != can be followed by a BOOL or STRING @@ -166,15 +226,7 @@ class DOMLRTransformer(Transformer): or attr(e1, rel, val) and get_int(val) >= NUMBER """ - print(args) - return args - - def rhs_const_attribute(self, args): - """Parse rhs of expression - ==, != followed by CONST RELATIONSHIP - should generate attr(e1, rel, val) and attr(e2, rel, val) and e1 COMP_OP e2 - """ - print(args) + print("rel_attr_elem_expr", args) return args def _get_equality_sides(self, arg1, arg2): @@ -210,49 +262,42 @@ class DOMLRTransformer(Transformer): self.const_store.use(args[0].value) return args[0] - # def comparison(self, args): - # def _gen_comparison(enc: SMTEncoding, sorts: SMTSorts): - # a = args[0](enc, sorts) - # b = args[2](enc, sorts) - # op = args[1].value - - # # To extract the `int` contained in the attr_data_sort, - # # we need to call its `get_int` method on the `DatatypeRef` - # get_int = sorts.attr_data_sort.get_int - - # # TODO: Find a way to check if we're actually comparing Integers? - - # a = get_int(a) - # b = get_int(b) - - # if op == ">": - # return a > b - # if op == ">=": - # return a >= b - # if op == "<": - # return a < b - # if op == "<=": - # return a <= b - # if op == "==": - # return a == b - # if op == "!=": - # return a != b - - # return _gen_comparison - - def value(self, args): + def compare_int(self, sorts: SMTSorts, op: str, a, b): + # To extract the `int` contained in the attr_data_sort, + # we need to call its `get_int` method on the `DatatypeRef` + get_int = sorts.attr_data_sort.get_int + + a = get_int(a) + b = get_int(b) + + if op == ">": + return a > b + if op == ">=": + return a >= b + if op == "<": + return a < b + if op == "<=": + return a <= b + if op == "==": + return a == b + if op == "!=": + return a != b + raise f"Invalid Compare Operator Symbol: {op}" + + + def value(self, args): type = args[0].type value = args[0].value if type == "ESCAPED_STRING": self.user_values_cache.add(value) - return lambda enc, sorts: RefHandler.get_str(value, enc, sorts) + return lambda enc, sorts: RefHandler.get_str(value, enc, sorts), RefHandler.STRING elif type == "NUMBER": - return lambda _, sorts: RefHandler.get_int(value, sorts) + return lambda _, sorts: RefHandler.get_int(value, sorts), RefHandler.INTEGER elif type == "BOOL": - return lambda _, sorts: RefHandler.get_bool(value, sorts) - elif type == "VALUE": - return lambda _, sorts: RefHandler.get_value(value, sorts) + return lambda _, sorts: RefHandler.get_bool(value, sorts), RefHandler.BOOLEAN + # elif type == "VALUE": + # return lambda _, sorts: RefHandler.get_value(value, sorts), RefHandler.VALUE_REF def error_desc(self, args): def err_callback( diff --git a/mc_openapi/doml_mc/domlr_parser/utils.py b/mc_openapi/doml_mc/domlr_parser/utils.py index 617649b39cd852faca88f963cdef6c3f102dc700..cf1c57acce3542be2460f9384cf9dd8a8016808c 100644 --- a/mc_openapi/doml_mc/domlr_parser/utils.py +++ b/mc_openapi/doml_mc/domlr_parser/utils.py @@ -85,6 +85,10 @@ class RefHandler: ASSOCIATION = 0 ATTRIBUTE = 1 + INTEGER = 2 + BOOLEAN = 3 + STRING = 4 + def get_relationship(enc: SMTEncoding, rel_name: str) -> tuple[DatatypeRef, int]: rel_name = _convert_rel_str(rel_name) rel = enc.associations.get(rel_name, None) diff --git a/tests/domlr/example_multiple_reqs.domlr b/tests/domlr/example_multiple_reqs.domlr index eaacc37c5ccfbefb702695f0f518eee3c9691ab7..31f6941053d95e122345d4bbd75823a935333ab2 100644 --- a/tests/domlr/example_multiple_reqs.domlr +++ b/tests/domlr/example_multiple_reqs.domlr @@ -7,17 +7,27 @@ error: "VM {vm} must have iface {iface}" -+ "VM must have iface" +# + "VM must have iface" +# forall vm ( +# vm is class infrastructure.VirtualMachine +# implies +# exists iface ( +# vm has infrastructure.ComputingNode.ifaces iface +# ) +# ) + +# error: "VM {vm} must have iface {iface}" + ++ "VM must have cpu_count >= 4" forall vm ( vm is class infrastructure.VirtualMachine implies - exists iface ( - vm has infrastructure.ComputingNode.ifaces iface - ) + vm has infrastructure.ComputingNode.cpu_count >= 4 ) - error: "VM {vm} must have iface {iface}" + error: "VM {vm} must have cpu_count >= 4 {iface}" +# OLD SYNTAX: # - "Iface must be unique" # ni1 has infrastructure.NetworkInterface.endPoint Value # and @@ -30,5 +40,4 @@ and ni1 is not ni2 - error: "Iface {ni1} and {ni2} must have different values"