#!/usr/bin/env python

"""Exposes functions to perform a source-to-source transformation
that detects and unrolls loops in the code being analyzed.
"""

"""See the LICENSE file, located in the root directory of
the source distribution and
at http://verifun.eecs.berkeley.edu/gametime/about/LICENSE,
for details on the GameTime license and authors.
"""


import os
import subprocess

from defaults import config, sourceDir


class HandlerMode(object):
    """Represents the mode that the loop handler works in."""

    #: Detect loops.
    DETECTOR = 0
    #: Unroll loops.
    UNROLLER = 1


def _generateHandlerCommand(projectConfig, handlerMode):
    """Generates the system call that runs the loop handler
    with appropriate inputs.

    Arguments:
        projectConfig:
            :class:`~gametime.projectConfiguration.ProjectConfiguration`
            object that represents the configuration of a GameTime project.
        handlerMode:
            Mode that the loop handler should run in.

    Returns:
        Appropriate system call as a list that contains the program
        to be run and the proper arguments.
    """
    # Set the environment variable that allows the Cilly driver to find
    # the path to the configuration file for the Findlib OCaml module.
    os.environ["OCAMLFIND_CONF"] = os.path.join(sourceDir,
                                                "ocaml/conf/findlib.conf")

    # Set the environment variable that allows the Cilly driver to find
    # the path to the folder that contains the compiled OCaml files.
    os.environ["OCAMLPATH"] = os.path.join(sourceDir, "ocaml/lib")

    # Set the environment variable that configures the Cilly driver to load
    # the features that will be needed for the loop handler.
    os.environ["CIL_FEATURES"] = "cil.default-features,loopHandler.loopHandler"

    command = []

    command.append(os.path.join(config.TOOL_CIL, "bin/cilly.bat"))

    command.append("--doloopHandler")
    command.append("--loopHandler-detect"
                   if handlerMode is HandlerMode.DETECTOR
                   else "--loopHandler-unroll")

    command.append("--loopHandler-analyze=%s" % projectConfig.func)
    loopConfigFile = os.path.join(projectConfig.locationTempDir,
                                  config.TEMP_LOOP_CONFIG)
    command.append("--loopHandler-config='%s'" % loopConfigFile)    

    for inlineName in projectConfig.inlined:
        command.append("--inline='%s'" % inlineName)

    analysisFile = ("%s%s.c" % (projectConfig.locationTempNoExtension,
                                config.TEMP_SUFFIX_LINE_NUMS)
                    if handlerMode is HandlerMode.DETECTOR
                    else projectConfig.locationTempFile)
    command.append(analysisFile)    

    command.append("-I'%s'" % projectConfig.locationOrigDir)
    command.append("--save-temps='%s'" % projectConfig.locationTempDir)
    command.append("-c")
    command.append("-o")
    command.append("'%s.out'" % projectConfig.locationTempNoExtension)

    return command

def runDetector(projectConfig):
    """Conducts the sequence of system calls that will detect loops
    for the function currently being analyzed. The output of the
    detector will be placed in a loop configuration file that the
    user has to modify: this file contains the line numbers of each
    loop header, and the user has to specify bounds for each loops
    by changing the number beside the line numbers, which is set to
    1 by default.

    Arguments:
        projectConfig:
            :class:`~gametime.projectConfiguration.ProjectConfiguration`
            object that represents the configuration of a GameTime project.

    Returns:
        Zero if the inlining was successful; a non-zero value otherwise.
    """
    command = _generateHandlerCommand(projectConfig, HandlerMode.DETECTOR)
    proc = subprocess.call(command, shell=True)
    return proc

def runUnroller(projectConfig):
    """Conducts the sequence of system calls that will unroll loops
    in the function currently being analyzed. The output of the
    detector will be a temporary file for GameTime analysis where
    all of the loops have been unrolled using user-specified bounds.

    Precondition: The loop detector has already been run, and the user
    has already specified bounds for each loop in the loop configuration
    file generated by the loop detector.

    Arguments:
        projectConfig:
            :class:`~gametime.projectConfiguration.ProjectConfiguration`
            object that represents the configuration of a GameTime project.

    Returns:
        Zero if the inlining was successful; a non-zero value otherwise.
    """
    command = _generateHandlerCommand(projectConfig, HandlerMode.UNROLLER)
    proc = subprocess.call(command, shell=True)
    return proc

#!/usr/bin/env python

"""Exposes functions to perform a source-to-source transformation
that detects and unrolls loops in the code being analyzed.
"""

"""See the LICENSE file, located in the root directory of
the source distribution and
at http://verifun.eecs.berkeley.edu/gametime/about/LICENSE,
for details on the GameTime license and authors.
"""


import os
import subprocess

from defaults import config, sourceDir


class HandlerMode(object):
    """Represents the mode that the loop handler works in."""

    #: Detect loops.
    DETECTOR = 0
    #: Unroll loops.
    UNROLLER = 1


def _generateHandlerCommand(projectConfig, handlerMode):
    """Generates the system call that runs the loop handler
    with appropriate inputs.

    Arguments:
        projectConfig:
            :class:`~gametime.projectConfiguration.ProjectConfiguration`
            object that represents the configuration of a GameTime project.
        handlerMode:
            Mode that the loop handler should run in.

    Returns:
        Appropriate system call as a list that contains the program
        to be run and the proper arguments.
    """
    # Set the environment variable that allows the Cilly driver to find
    # the path to the configuration file for the Findlib OCaml module.
    os.environ["OCAMLFIND_CONF"] = os.path.join(sourceDir,
                                                "ocaml/conf/findlib.conf")

    # Set the environment variable that allows the Cilly driver to find
    # the path to the folder that contains the compiled OCaml files.
    os.environ["OCAMLPATH"] = os.path.join(sourceDir, "ocaml/lib")

    # Set the environment variable that configures the Cilly driver to load
    # the features that will be needed for the loop handler.
    os.environ["CIL_FEATURES"] = "cil.default-features,loopHandler.loopHandler"

    command = []

    command.append(os.path.join(config.TOOL_CIL, "bin/cilly.bat"))

    command.append("--doloopHandler")
    command.append("--loopHandler-detect"
                   if handlerMode is HandlerMode.DETECTOR
                   else "--loopHandler-unroll")

    command.append("--loopHandler-analyze=%s" % projectConfig.func)
    loopConfigFile = os.path.join(projectConfig.locationTempDir,
                                  config.TEMP_LOOP_CONFIG)
    command.append("--loopHandler-config='%s'" % loopConfigFile)    

    for inlineName in projectConfig.inlined:
        command.append("--inline='%s'" % inlineName)

    analysisFile = ("%s%s.c" % (projectConfig.locationTempNoExtension,
                                config.TEMP_SUFFIX_LINE_NUMS)
                    if handlerMode is HandlerMode.DETECTOR
                    else projectConfig.locationTempFile)
    command.append(analysisFile)    

    command.append("-I'%s'" % projectConfig.locationOrigDir)
    command.append("--save-temps='%s'" % projectConfig.locationTempDir)
    command.append("-c")
    command.append("-o")
    command.append("'%s.out'" % projectConfig.locationTempNoExtension)

    return command

def runDetector(projectConfig):
    """Conducts the sequence of system calls that will detect loops
    for the function currently being analyzed. The output of the
    detector will be placed in a loop configuration file that the
    user has to modify: this file contains the line numbers of each
    loop header, and the user has to specify bounds for each loops
    by changing the number beside the line numbers, which is set to
    1 by default.

    Arguments:
        projectConfig:
            :class:`~gametime.projectConfiguration.ProjectConfiguration`
            object that represents the configuration of a GameTime project.

    Returns:
        Zero if the inlining was successful; a non-zero value otherwise.
    """
    command = _generateHandlerCommand(projectConfig, HandlerMode.DETECTOR)
    proc = subprocess.call(command, shell=True)
    return proc

def runUnroller(projectConfig):
    """Conducts the sequence of system calls that will unroll loops
    in the function currently being analyzed. The output of the
    detector will be a temporary file for GameTime analysis where
    all of the loops have been unrolled using user-specified bounds.

    Precondition: The loop detector has already been run, and the user
    has already specified bounds for each loop in the loop configuration
    file generated by the loop detector.

    Arguments:
        projectConfig:
            :class:`~gametime.projectConfiguration.ProjectConfiguration`
            object that represents the configuration of a GameTime project.

    Returns:
        Zero if the inlining was successful; a non-zero value otherwise.
    """
    command = _generateHandlerCommand(projectConfig, HandlerMode.UNROLLER)
    proc = subprocess.call(command, shell=True)
    return proc

#!/usr/bin/env python Exposes functions to perform a source-to-source transformation that detects and unrolls loops in the code being analyzed. See the LICENSE file, located in the root directory of the source distribution and at http://verifun.eecs.berkeley.edu/gametime/about/LICENSE, for details on the GameTime license and authors. Represents the mode that the loop handler works in. #: Detect loops. #: Unroll loops. Generates the system call that runs the loop handler     with appropriate inputs.      Arguments:         projectConfig:             :class:`~gametime.projectConfiguration.ProjectConfiguration`             object that represents the configuration of a GameTime project.         handlerMode:             Mode that the loop handler should run in.      Returns:         Appropriate system call as a list that contains the program         to be run and the proper arguments. # Set the environment variable that allows the Cilly driver to find # the path to the configuration file for the Findlib OCaml module. # Set the environment variable that allows the Cilly driver to find # the path to the folder that contains the compiled OCaml files. # Set the environment variable that configures the Cilly driver to load # the features that will be needed for the loop handler. Conducts the sequence of system calls that will detect loops     for the function currently being analyzed. The output of the     detector will be placed in a loop configuration file that the     user has to modify: this file contains the line numbers of each     loop header, and the user has to specify bounds for each loops     by changing the number beside the line numbers, which is set to     1 by default.      Arguments:         projectConfig:             :class:`~gametime.projectConfiguration.ProjectConfiguration`             object that represents the configuration of a GameTime project.      Returns:         Zero if the inlining was successful; a non-zero value otherwise. Conducts the sequence of system calls that will unroll loops     in the function currently being analyzed. The output of the     detector will be a temporary file for GameTime analysis where     all of the loops have been unrolled using user-specified bounds.      Precondition: The loop detector has already been run, and the user     has already specified bounds for each loop in the loop configuration     file generated by the loop detector.      Arguments:         projectConfig:             :class:`~gametime.projectConfiguration.ProjectConfiguration`             object that represents the configuration of a GameTime project.      Returns:         Zero if the inlining was successful; a non-zero value otherwise.