# vim: set sw=2 ts=2 softtabstop=2 expandtab:
from . RunnerBase import RunnerBaseClass
from .. ResultType import ResultType
from .. Analysers.GPUVerify import GPUVerifyAnalyser
import logging
import os
import psutil
import re
import sys
import yaml

_logger = logging.getLogger(__name__)

class GPUVerifyRunnerException(Exception):
  def __init__(self, msg):
    self.msg = msg

class GPUVerifyRunner(RunnerBaseClass):
  softTimeoutDiff = 5

  def __init__(self, boogieProgram, workingDirectory, rc):
    _logger.debug('Initialising {}'.format(boogieProgram))
    super(GPUVerifyRunner, self).__init__(boogieProgram, workingDirectory, rc)

    # Sanity checks
    # TODO

    if self.maxTimeInSeconds > 0 and (
       self.maxTimeInSeconds <= self.softTimeoutDiff):
      raise GPUVerifyRunnerException('Need larger timeout')

    if not self.toolPath.endswith('.py'):
      raise GPUVerifyRunnerException(
        'toolPath needs to be the GPUVerify python script')

  @property
  def name(self):
    return "gpuverify"

  @property
  def timeoutWasHit(self):
    if self.hitHardTimeout:
      return True
    else:
      if self.exitCode == 7:
        return True
      else:
        return False

  def getResults(self):
    results = super(GPUVerifyRunner, self).getResults()
    results['hit_hard_timeout'] = self.hitHardTimeout
    return results

  def GetNewAnalyser(self):
    return GPUVerifyAnalyser(self.exitCode, self.logFile, self.useDocker, self.hitHardTimeout)

  def run(self):
    self.hitHardTimeout = False

    # Run using python interpreter
    cmdLine = [ sys.executable, self.toolPath ]

    # Set a soft timeout
    softTimeout = self.maxTimeInSeconds - self.softTimeoutDiff
    cmdLine.append('--timeout={}'.format(softTimeout))


    # Note we ignore self.entryPoint

    # GPUVerify needs PATH environment variable set
    env = {}
    path = os.getenv('PATH')
    if path == None:
      path = ""

    env['PATH'] = path

    cmdLine.extend(self.additionalArgs)

    # Add the boogie source file as last arg
    cmdLine.append(self.programPathArgument)

    try:
      exitCode = self.runTool(cmdLine,
        isDotNet=False,
        envExtra=env)
      assert self.exitCode == exitCode
    except psutil.TimeoutExpired as e:
      self.hitHardTimeout = True
      _logger.warning('GPUVerify hit hard timeout')

def get():
  return GPUVerifyRunner

# vim: set sw=2 ts=2 softtabstop=2 expandtab:
from . RunnerBase import RunnerBaseClass
from .. ResultType import ResultType
from .. Analysers.GPUVerify import GPUVerifyAnalyser
import logging
import os
import psutil
import re
import sys
import yaml

_logger = logging.getLogger(__name__)

class GPUVerifyRunnerException(Exception):
  def __init__(self, msg):
    self.msg = msg

class GPUVerifyRunner(RunnerBaseClass):
  softTimeoutDiff = 5

  def __init__(self, boogieProgram, workingDirectory, rc):
    _logger.debug('Initialising {}'.format(boogieProgram))
    super(GPUVerifyRunner, self).__init__(boogieProgram, workingDirectory, rc)

    # Sanity checks
    # TODO

    self.softTimeout = self.maxTimeInSeconds
    if self.maxTimeInSeconds > 0:
      # We use GPUVerify's timeout function and enforce the
      # requested timeout and enforce a hard timeout slightly later
      self.maxTimeInSeconds = self.maxTimeInSeconds + self.softTimeoutDiff

    if not self.toolPath.endswith('.py'):
      raise GPUVerifyRunnerException(
        'toolPath needs to be the GPUVerify python script')

  @property
  def name(self):
    return "gpuverify"

  @property
  def timeoutWasHit(self):
    if self.hitHardTimeout:
      return True
    else:
      if self.exitCode == 7:
        return True
      else:
        return False

  def getResults(self):
    results = super(GPUVerifyRunner, self).getResults()
    results['hit_hard_timeout'] = self.hitHardTimeout
    return results

  def GetNewAnalyser(self):
    return GPUVerifyAnalyser(self.exitCode, self.logFile, self.useDocker, self.hitHardTimeout)

  def run(self):
    self.hitHardTimeout = False

    # Run using python interpreter
    cmdLine = [ sys.executable, self.toolPath ]

    cmdLine.append('--timeout={}'.format(self.softTimeout))

    # Note we ignore self.entryPoint
    _logger.info('Ignoring entry point {}'.format(self.entryPoint))

    # GPUVerify needs PATH environment variable set
    env = {}
    path = os.getenv('PATH')
    if path == None:
      path = ""

    env['PATH'] = path

    cmdLine.extend(self.additionalArgs)

    # Add the boogie source file as last arg
    cmdLine.append(self.programPathArgument)

    try:
      exitCode = self.runTool(cmdLine,
        isDotNet=False,
        envExtra=env)
      assert self.exitCode == exitCode
    except psutil.TimeoutExpired as e:
      self.hitHardTimeout = True
      _logger.warning('GPUVerify hit hard timeout')

def get():
  return GPUVerifyRunner

Change timeout behaviour for GPUVerify to make it slightly fairer. We pass the GPUVerify ``--timeout=`` parameter the requested time and enforce a hard timeout slightly later. Before we were giving GPUVerify 5 seconds less than the other tools which wasn't fair.