Add requirement from issue #25 on GitLab (asg->vm)

docs/requirements.rst

@@ -73,6 +73,7 @@ ID: ``all_concrete_map_something``
 
 Makes sure each concrete infrastructure element is mapped to a node in the Abstract Infrastructure Layer.
 
+
 Network Interfaces belong to a Security Group
 ---------------------------------------------
 
@@ -83,11 +84,26 @@ ID: ``security_group_must_have_iface``
 Makes sure all network interfaces have been configured to belong to a security group.
 This way, the user will be reminded to configure adequate rules for each network.
 
-External Services are reached through HTTPS
--------------------------------------------
 
-  All external SaaS can be reached only through a secure connection.
+Virtual Machines in AutoScaleGroup should not be present in Concretization
+--------------------------------------------------------------------------
+
+ID: ``concrete_asg_no_vm``
+
+*Available from DOML v2.2+*
+
+Makes sure a VM present inside an AutoScaleGroup in the Infrastructure Layer is not present
+and mapped in the Concretization layer.
+
+
+.. Deprecated
+
+.. External Services are reached through HTTPS
+.. -------------------------------------------
+
+..   All external SaaS can be reached only through a secure connection.
+
+.. ID: ``external_services_must_have_https``
 
-ID: ``external_services_must_have_https``
+.. Makes sure that an HTTPS rule is enforced for a Network Interface of a Software Component that interfaces with a SaaS.
 
-Makes sure that an HTTPS rule is enforced for a Network Interface of a Software Component that interfaces with a SaaS.
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/__init__.py

@@ -4,7 +4,7 @@ CELEMS_V2_0 = [
     ("infrastructure_Network", "concrete_RuntimeProvider::networks", "concrete_Network::maps"),
     ("infrastructure_Storage", "concrete_RuntimeProvider::storages", "concrete_Storage::maps"),
     ("infrastructure_FunctionAsAService", "concrete_RuntimeProvider::faas","concrete_FunctionAsAService::maps"),
-    ("infrastructure_ComputingGroup", "concrete_RuntimeProvider::group","concrete_ComputingGroup::maps")
+    ("infrastructure_ComputingGroup", "concrete_RuntimeProvider::group","concrete_ComputingGroup::maps"),
 ]
 
 from .vm_has_iface import VM_HAS_IFACE, VM_HAS_IFACE_V2_3
@@ -14,6 +14,7 @@ from .all_software_components_deployed import ALL_SOFTWARE_COMPONENTS_DEPLOYED
 from .all_infrastructure_elements_deployed import ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED
 from .all_concrete_maps_something import ALL_CONCRETE_MAP_SOMETHING
 from .security_group_must_have_iface import SECURITY_GROUP_MUST_HAVE_IFACE
+from .concrete_asg_no_vm import CONCRETE_ASG_NO_VM
 
 __ALL__ = [
     VM_HAS_IFACE,
@@ -25,5 +26,6 @@ __ALL__ = [
     ALL_SOFTWARE_COMPONENTS_DEPLOYED,
     ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
     ALL_CONCRETE_MAP_SOMETHING,
-    SECURITY_GROUP_MUST_HAVE_IFACE
+    SECURITY_GROUP_MUST_HAVE_IFACE,
+    CONCRETE_ASG_NO_VM
 ]
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py

@@ -45,8 +45,28 @@ def all_infrastructure_elements_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts
                     ielemClass, providerAssoc, celemAssoc
                 ) 
                 for ielemClass, providerAssoc, celemAssoc in CELEMS_V2_0
-                if ielemClass != 'infrastructure_VirtualMachine' # handle special case separately below
+                if ielemClass != 'infrastructure_VirtualMachine' # handle special case separately in concrete_asg_no_vm and below
             ),
+            And(
+                smtenc.element_class_fun(ielem) == smtenc.classes["infrastructure_VirtualMachine"],
+                Not(Exists([asg],
+                    Or(
+                        smtenc.association_rel(
+                            asg, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], ielem),
+                        Exists(
+                            [provider, celem],
+                            And(
+                                smtenc.association_rel(
+                                    concr, smtenc.associations["concrete_ConcreteInfrastructure::providers"], provider),
+                                smtenc.association_rel(
+                                    provider, smtenc.associations["concrete_RuntimeProvider::vms"], celem),
+                                smtenc.association_rel(
+                                    celem, smtenc.associations["concrete_VirtualMachine::maps"], ielem)
+                            )
+                        )
+                    )
+                ))
+            )
         )
     )
 

mc_openapi/doml_mc/builtin_requirements/concrete_asg_no_vm.py

+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+
+def concrete_asg_no_vm(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    ielem, concr, provider, celem, asg = Consts("ielem concr provider celem asg", smtsorts.element_sort)
+    return And(
+        smtenc.element_class_fun(
+            concr) == smtenc.classes["concrete_ConcreteInfrastructure"],
+        # We don't want the following to happen:
+        # If exists ASG(infr) -> VM(infr), then exists a VM(concr) -> VM(infr) 
+        And(
+            smtenc.element_class_fun(ielem) == smtenc.classes["infrastructure_VirtualMachine"],
+            smtenc.association_rel(
+                asg, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], ielem),
+            (Exists(
+                [celem],
+                smtenc.association_rel(celem, smtenc.associations["concrete_VirtualMachine::maps"], ielem)
+            ))
+        )
+    )
+
+
+def ed_concrete_asg_no_vm(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    try:
+        ielem = Const("ielem", smtsorts.element_sort)
+        asg = Const("asg", smtsorts.element_sort)
+        ielem_name = get_user_friendly_name(
+            intermediate_model, solver.model(), ielem)
+        if ielem_name:
+            return f"Virtual machine '{ielem_name}' in AutoScale Group '{asg}' should not be present in the concretization layer."
+    except:
+        return "Any virtual machine in an AutoScale Group should not be present in the concretization layer."
+
+MSG = "All virtual machines in an autoscale group in the infrastructure layer should not be mapped in the concretization layer."
+
+CONCRETE_ASG_NO_VM = (
+    concrete_asg_no_vm,
+    "concrete_asg_no_vm",
+    MSG,
+    ed_concrete_asg_no_vm
+)
\ No newline at end of file

mc_openapi/doml_mc/common_reqs.py

@@ -29,7 +29,8 @@ REQUIREMENTS = {
         ALL_SOFTWARE_COMPONENTS_DEPLOYED,
         ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
         ALL_CONCRETE_MAP_SOMETHING,
-        SECURITY_GROUP_MUST_HAVE_IFACE
+        SECURITY_GROUP_MUST_HAVE_IFACE,
+        CONCRETE_ASG_NO_VM
     ],
     DOMLVersion.V2_3: [
         VM_HAS_IFACE_V2_3,
@@ -38,7 +39,8 @@ REQUIREMENTS = {
         ALL_SOFTWARE_COMPONENTS_DEPLOYED,
         ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
         ALL_CONCRETE_MAP_SOMETHING,
-        SECURITY_GROUP_MUST_HAVE_IFACE
+        SECURITY_GROUP_MUST_HAVE_IFACE,
+        CONCRETE_ASG_NO_VM
     ],
 }
 

tests/test_modelchecker.py

@@ -56,13 +56,13 @@ OUTPUT = {
     'v2.2': {
         'faas.domlx': 'unsat',
         'iot_simple_app.domlx': 'unsat',
-        'nginx-aws-ec2.domlx': 'sat',
+        'nginx-aws-ec2.domlx': 'unsat', # was sat before concrete_asg_no_vm req
         'nginx_func_req2_unsat.domlx': 'unsat',
         'nginx_func_req2_unsat_neg.domlx': 'unsat',
-        'nginx_func_req_neg.domlx': 'sat',
-        'nginx-csp-compatibility-test.domlx': 'sat',
-        'nginx_func_req.domlx': 'sat',
-        'nginx_flags.domlx': 'sat'
+        'nginx_func_req_neg.domlx': 'unsat', # ditto
+        'nginx-csp-compatibility-test.domlx': 'unsat', # ditto
+        'nginx_func_req.domlx': 'unsat', # ditto
+        'nginx_flags.domlx': 'unsat' # ditto
     },
     'v2.3': {