Array index analysis using SMT

setup.py

@@ -170,7 +170,8 @@ def get_files(directory, install_path, valid_suffixes):
         packages=PACKAGES,
         package_dir={"": "src"},
         install_requires=['pyparsing', 'fparser>=0.2.1', 'configparser',
-                          'sympy', "Jinja2", 'termcolor', 'graphviz'],
+                          'sympy', "Jinja2", 'termcolor', 'graphviz',
+                          'z3-solver'],
         extras_require={
             'doc': ["sphinx", "sphinxcontrib.bibtex", "sphinx_design",
                     "pydata-sphinx-theme", "sphinx-autodoc-typehints",

src/psyclone/psyir/tools/__init__.py

@@ -43,11 +43,15 @@
 from psyclone.psyir.tools.read_write_info import ReadWriteInfo
 from psyclone.psyir.tools.definition_use_chains import DefinitionUseChain
 from psyclone.psyir.tools.reduction_inference import ReductionInferenceTool
+from psyclone.psyir.tools.array_index_analysis import (ArrayIndexAnalysis,
+    ArrayIndexAnalysisOptions)
 
 # For AutoAPI documentation generation.
 __all__ = ['CallTreeUtils',
            'DTCode',
            'DependencyTools',
            'DefinitionUseChain', 
            'ReadWriteInfo',
-           'ReductionInferenceTool']
+           'ReductionInferenceTool',
+           'ArrayIndexAnalysis',
+           'ArrayIndexAnalysisOptions']

src/psyclone/psyir/tools/dependency_tools.py

@@ -50,6 +50,8 @@
 from psyclone.psyir.backend.sympy_writer import SymPyWriter
 from psyclone.psyir.backend.visitor import VisitorError
 from psyclone.psyir.nodes import Loop, Node, Range
+from psyclone.psyir.tools.array_index_analysis import (
+    ArrayIndexAnalysis, ArrayIndexAnalysisOptions)
 
 
 # pylint: disable=too-many-lines
@@ -162,11 +164,20 @@ class DependencyTools():
         specified in the PSyclone config file. This can be used to
         exclude for example 1-dimensional loops.
     :type loop_types_to_parallelise: Optional[List[str]]
+    :param use_smt_array_index_analysis: if True, the SMT-based
+        array index analysis will be used for detecting array access
+        conflicts. An ArrayIndexAnalysisOptions value can also be given,
+        instead of a bool, in which case the analysis will be invoked
+        with the given options.
+    :type use_smt_array_index_analysis: Union[
+        bool, ArrayIndexAnalysisOptions]
 
     :raises TypeError: if an invalid loop type is specified.
 
     '''
-    def __init__(self, loop_types_to_parallelise=None):
+    def __init__(self,
+                 loop_types_to_parallelise=None,
+                 use_smt_array_index_analysis=False):
         if loop_types_to_parallelise:
             # Verify that all loop types specified are valid:
             config = Config.get()
@@ -183,6 +194,7 @@ def __init__(self, loop_types_to_parallelise=None):
         else:
             self._loop_types_to_parallelise = []
         self._clear_messages()
+        self._use_smt_array_index_analysis = use_smt_array_index_analysis
 
     # -------------------------------------------------------------------------
     def _clear_messages(self):
@@ -884,9 +896,15 @@ def can_loop_be_parallelised(self, loop,
             # TODO #1270 - the is_array_access function might be moved
             is_array = symbol.is_array_access(access_info=var_info)
             if is_array:
-                # Handle arrays
-                par_able = self._array_access_parallelisable(loop_vars,
-                                                             var_info)
+                # If using the SMT-based array index analysis then do
+                # nothing for now. This analysis is run after the loop.
+                if self._use_smt_array_index_analysis:
+                    # This analysis runs after the loop
+                    par_able = True
+                else:
+                    # Handle arrays
+                    par_able = self._array_access_parallelisable(loop_vars,
+                                                                 var_info)
             else:
                 # Handle scalar variable
                 par_able = self._is_scalar_parallelisable(signature, var_info)
@@ -898,6 +916,23 @@ def can_loop_be_parallelised(self, loop,
                 # not just the first one
                 result = False
 
+        # Apply the SMT-based array index analysis, if enabled
+        if self._use_smt_array_index_analysis:
+            if isinstance(self._use_smt_array_index_analysis,
+                          ArrayIndexAnalysisOptions):
+                options = self._use_smt_array_index_analysis
+            else:
+                options = ArrayIndexAnalysisOptions()
+            analysis = ArrayIndexAnalysis(options)
+            conflict_free = analysis.is_loop_conflict_free(loop)
+            if not conflict_free:
+                self._add_message(
+                    "The ArrayIndexAnalysis has determined that the"
+                    "array accesses in the loop may be conflicting "
+                    "and hence cannot be parallelised.",
+                    DTCode.ERROR_DEPENDENCY)
+                result = False
+
         return result
 
 # -------------------------------------------------------------------------

src/psyclone/psyir/transformations/parallel_loop_trans.py

@@ -53,7 +53,8 @@
         BinaryOperation, IntrinsicCall
 )
 from psyclone.psyir.tools import (
-        DependencyTools, DTCode, ReductionInferenceTool
+        DependencyTools, DTCode, ReductionInferenceTool,
+        ArrayIndexAnalysisOptions
 )
 from psyclone.psyir.transformations.loop_trans import LoopTrans
 from psyclone.psyir.transformations.async_trans_mixin import \
@@ -175,6 +176,8 @@ def validate(self, node, options=None, **kwargs):
             reduction_ops = self.get_option("reduction_ops", **kwargs)
             if reduction_ops is None:
                 reduction_ops = []
+            use_smt_array_index_analysis = self.get_option(
+                "use_smt_array_index_analysis", **kwargs)
         else:
             verbose = options.get("verbose", False)
             collapse = options.get("collapse", False)
@@ -185,6 +188,8 @@ def validate(self, node, options=None, **kwargs):
             sequential = options.get("sequential", False)
             privatise_arrays = options.get("privatise_arrays", False)
             reduction_ops = options.get("reduction_ops", [])
+            use_smt_array_index_analysis = options.get(
+                "use_smt_array_index_analysis", False)
 
         # Check type of reduction_ops (not handled by validate_options)
         if not isinstance(reduction_ops, list):
@@ -260,7 +265,8 @@ def validate(self, node, options=None, **kwargs):
                     f" object containing str representing the "
                     f"symbols to ignore, but got '{ignore_dependencies_for}'.")
 
-        dep_tools = DependencyTools()
+        dep_tools = DependencyTools(
+            use_smt_array_index_analysis=use_smt_array_index_analysis)
 
         signatures = [Signature(name) for name in ignore_dependencies_for]
 
@@ -326,6 +332,8 @@ def apply(self, node, options=None, verbose: bool = False,
               nowait: bool = False,
               reduction_ops: List[Union[BinaryOperation.Operator,
                                         IntrinsicCall.Intrinsic]] = None,
+              use_smt_array_index_analysis:
+                  Union[bool, ArrayIndexAnalysisOptions] = False,
               **kwargs):
         '''
         Apply the Loop transformation to the specified node in a
@@ -370,6 +378,11 @@ def apply(self, node, options=None, verbose: bool = False,
         :param reduction_ops: if non-empty, attempt parallelisation
             of loops by inferring reduction clauses involving any of
             the reduction operators in the list.
+        :param use_smt_array_index_analysis: if True, the SMT-based
+            array index analysis will be used for detecting array access
+            conflicts. An ArrayIndexAnalysisOptions value can also be given,
+            instead of a bool, in which case the analysis will be invoked
+            with the given options.
 
         '''
         if not options:
@@ -378,7 +391,9 @@ def apply(self, node, options=None, verbose: bool = False,
                     ignore_dependencies_for=ignore_dependencies_for,
                     privatise_arrays=privatise_arrays,
                     sequential=sequential, nowait=nowait,
-                    reduction_ops=reduction_ops, **kwargs
+                    reduction_ops=reduction_ops,
+                    use_smt_array_index_analysis=use_smt_array_index_analysis,
+                    **kwargs
             )
             # Rename the input options that are renamed in this apply method.
             # TODO 2668, rename options to be consistent.
@@ -399,16 +414,22 @@ def apply(self, node, options=None, verbose: bool = False,
             privatise_arrays = options.get("privatise_arrays", False)
             nowait = options.get("nowait", False)
             reduction_ops = options.get("reduction_ops", [])
+            use_smt_array_index_analysis = options.get(
+                "use_smt_array_index_analysis", False)
 
         self.validate(node, options=options, verbose=verbose,
                       collapse=collapse, force=force,
                       ignore_dependencies_for=ignore_dependencies_for,
                       privatise_arrays=privatise_arrays,
                       sequential=sequential, nowait=nowait,
-                      reduction_ops=reduction_ops, **kwargs)
+                      reduction_ops=reduction_ops,
+                      use_smt_array_index_analysis=(
+                          use_smt_array_index_analysis),
+                      **kwargs)
 
         list_of_signatures = [Signature(name) for name in list_of_names]
-        dtools = DependencyTools()
+        dtools = DependencyTools(
+                   use_smt_array_index_analysis=use_smt_array_index_analysis)
 
         # Add all reduction variables inferred by 'validate' to the list
         # of signatures to ignore

src/psyclone/tests/psyir/nodes/omp_directives_test.py

@@ -5349,3 +5349,41 @@ def test_firstprivate_with_uninitialised(fortran_reader, fortran_writer):
     output = fortran_writer(psyir)
     assert "firstprivate(a)" in output
     assert "firstprivate(b)" in output
+
+
+def test_array_analysis_option(fortran_reader, fortran_writer):
+    '''Test that a tiled loop can be parallelised when using the SMT-based
+    array index analysis.
+    '''
+    psyir = fortran_reader.psyir_from_source('''
+      subroutine my_matmul(a, b, c)
+        integer, dimension(:,:), intent(in) :: a
+        integer, dimension(:,:), intent(in) :: b
+        integer, dimension(:,:), intent(out) :: c
+        integer :: x, y, k, k_out_var, x_out_var, y_out_var, a1_n, a2_n, b1_n
+
+        a2_n = SIZE(a, 2)
+        b1_n = SIZE(b, 1)
+        a1_n = SIZE(a, 1)
+
+        c(:,:) = 0
+        do y_out_var = 1, a2_n, 8
+          do x_out_var = 1, b1_n, 8
+            do k_out_var = 1, a1_n, 8
+              do y = y_out_var, MIN(y_out_var + (8 - 1), a2_n), 1
+                do x = x_out_var, MIN(x_out_var + (8 - 1), b1_n), 1
+                  do k = k_out_var, MIN(k_out_var + (8 - 1), a1_n), 1
+                    c(x,y) = c(x,y) + a(k,y) * b(x,k)
+                  enddo
+                enddo
+              enddo
+            enddo
+          enddo
+        enddo
+      end subroutine my_matmul''')
+    omplooptrans = OMPLoopTrans(omp_directive="paralleldo")
+    loop = psyir.walk(Loop)[0]
+    omplooptrans.apply(
+        loop, collapse=True, use_smt_array_index_analysis=True)
+    output = fortran_writer(psyir)
+    assert "collapse(2)" in output