#!/usr/bin/env python

"""
Try and parse counterexamples from histogram kernel
"""

import getopt
import io
import re
import sys

def threadPos(t):
  return ((t & (~63)) | ((t & 15) << 2) | ((t & 48) >> 4))

def print_cex_models(filename, THREAD_N, encoding='utf-16'):

  def accesspattern(threadPos, data):
    ds = [ ((data>>shift) & 0x3f) for shift in [26,18,10,2] ]
    return [ (threadPos + (d * THREAD_N)) for d in ds ]

  if encoding == 'utf-16':
    f = io.open(filename, 'rU', encoding='utf-16')
  else: #assume ascii
    f = open(filename, 'rU')

  for linenum, line in enumerate(f.readlines()):
    if line.find('*** MODEL') != -1:
      model_begin = linenum
      t1, t2, t1data, t2data = None, None, [], []
    if line.find('*** END_MODEL') != -1:
      if t1 == None or t2 == None:
        raise Exception("Bad model, lines %d to %d" % (model_begin, linenum))
      tP1, tP2 = threadPos(t1), threadPos(t2)
      t1access, t2access = [], []
      for data in t1data: t1access.extend(accesspattern(tP1, data))
      for data in t2data: t2access.extend(accesspattern(tP2, data))
      t1access, t2access = set(t1access), set(t2access)
      clash = t1access.intersection(t2access)
      print "-" * 80
      print "t1: tid %d with threadPos %d" % (t1, tP1)
      print "t1 accesses: ", sorted(t1access)
      print "t2: tid %d with threadPos %d" % (t2, tP2)
      print "t2 accesses: ", sorted(t2access)
      print "clash: ", sorted(clash)
    if line.find('local_id_x') != -1:
      m = re.search(r'local_id_x\$(?P<tid>[12]) -> (?P<val>[0-9]+)', line)
      tid = int(m.group('tid'))
      val = int(m.group('val'))
      if tid == 1:   t1 = val
      elif tid == 2: t2 = val
    if line.find('data4') != -1:
      m = re.search(r'[$]*(?P<name>[^.]+)\.[01]\$(?P<tid>[12])@[01] -> (?P<val>[0-9]+)', line)
      assert m.group('name') == 'data4'
      tid = int(m.group('tid'))
      val = int(m.group('val'))
      if tid == 1:   t1data.append(val)
      if tid == 2:   t2data.append(val)

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

def print_help(progname):
  print 'Usage: %s <cex.file>\n' % progname
  print 'Options:'
  print '  -h or --help'
  print '  -N or --thread_n=x    THREAD_N / blocksize (default=128)'
  print '  -e x or --encoding=x  Encoding of counterexample file'
  print '                        ascii or utf-16 (default) supported'
  print 'Generate cex.txt by passing /printModel:4 to Boogie'
  print 'and piping the output to a file'

def main(argv=None):
  if argv is None:
    argv = sys.argv
  progname = argv[0]
  try:
    try:
      opts, args = getopt.getopt(argv[1:],'he:N:',['help','encoding=','thread_n='])
    except getopt.error, msg:
      raise Usage(msg)
    THREAD_N = 128
    encoding = 'utf-16'
    for o, a in opts:
      if o in ('-h', '--help'):
        print_help(progname)
        return 0
      if o in ('-e', '--encoding'):
        encoding = a
        if encoding not in [ 'ascii', 'utf-16' ]:
          raise Usage('Error: unexpected encoding. Use ascii or utf-16.')
      if o in ('-N', '--thread_n'):
        THREAD_N = int(a)
    if len(args) != 1:
      raise Usage('Error: expecting exactly one counterexample file')
    print_cex_models(args[0],THREAD_N,encoding)
    return 0
  except Usage, err:
    print >>sys.stderr, err.msg
    print >>sys.stderr, 'Try --help for options'
    return 2
  except UnicodeError:
    print >>sys.stderr, 'Error with encoding [%s]' % encoding
    print >>sys.stderr, 'Try --help for options'
    return 2

if __name__ == '__main__':
  sys.exit(main())
