verigraph/service/src/tests/j-verigraph-generator/test_generator.py

   1 #!/usr/bin/python
   2
   3 ##############################################################################
   4 # Copyright (c) 2017 Politecnico di Torino and others.
   5 #
   6 # All rights reserved. This program and the accompanying materials
   7 # are made available under the terms of the Apache License, Version 2.0
   8 # which accompanies this distribution, and is available at
   9 # http://www.apache.org/licenses/LICENSE-2.0
  10 ##############################################################################
  11
  12 from pprint import pprint
  13 from code_generator import CodeGeneratorBackend
  14 import sys, getopt
  15 import contextlib
  16 import os
  17 from utility import *
  18 import logging
  19
  20 def main(argv):
  21     if len(argv) < 8:
  22         print 'test_generator.py -i <inputfile> -o <outputfile> -s <source> -d <destination>'
  23         sys.exit(2)
  24     #initialize command line arguments values
  25     inputfile = ''
  26     outputfile = ''
  27     source = ''
  28     destination = ''
  29     #parse command line arguments and exit if there is an error
  30     try:
  31         opts, args = getopt.getopt(argv,"hi:o:s:d:",["ifile=","ofile=","source=","destination="])
  32     except getopt.GetoptError:
  33         print 'test_generator.py -i <inputfile> -o <outputfile> -s <source> -d <destination>'
  34         sys.exit(2)
  35     for opt, arg in opts:
  36         if opt == '-h':
  37             print 'test_generator.py -i <inputfile> -o <outputfile> -s <source> -d <destination>'
  38             sys.exit()
  39         elif opt in ("-i", "--ifile"):
  40             inputfile = arg
  41         elif opt in ("-o", "--ofile"):
  42             outputfile = arg
  43         elif opt in ("-s", "--source"):
  44             source = arg
  45         elif opt in ("-d", "--destination"):
  46             destination = arg
  47     #set logging
  48     logging.basicConfig(stream=sys.stderr, level=logging.INFO)
  49     #capitalize ouput filename
  50     dirname = os.path.dirname(outputfile)
  51     basename = os.path.basename(outputfile)
  52     basename = os.path.splitext(basename)[0]
  53     basename = basename[0].upper() + basename[1:]
  54
  55     #print arguments
  56     logging.debug('Input file is', inputfile)
  57     logging.debug('Output file is', dirname + "/" + basename)
  58     logging.debug('Source node is', source)
  59     logging.debug('Destination node is', destination)
  60
  61     #begin file generation
  62     with smart_open(dirname + "/" + basename + ".java") as f:
  63         c = CodeGeneratorBackend()
  64         c.begin(tab="    ")
  65         c.writeln("package tests;")
  66         c.writeln("import java.util.Calendar;")
  67         c.writeln("import java.util.Date;")
  68         c.writeln("import java.util.HashMap;")
  69
  70         c.writeln("import com.microsoft.z3.Context;")
  71         c.writeln("import com.microsoft.z3.FuncDecl;")
  72         c.writeln("import com.microsoft.z3.Model;")
  73         c.writeln("import com.microsoft.z3.Status;")
  74         c.writeln("import com.microsoft.z3.Z3Exception;")
  75         c.writeln("import mcnet.components.IsolationResult;")
  76
  77
  78         inputfile = os.path.basename(inputfile)
  79         c.writeln("import tests.scenarios." + os.path.splitext(inputfile)[0] + ";")
  80         c.writeln("public class " + basename + "{")
  81
  82         c.indent()
  83         c.writeln("Context ctx;")
  84
  85         c.write("public void resetZ3() throws Z3Exception{\n\
  86         HashMap<String, String> cfg = new HashMap<String, String>();\n\
  87         cfg.put(\"model\", \"true\");\n\
  88         ctx = new Context(cfg);\n\
  89         \r\t}\n")
  90
  91         c.write("public void printVector (Object[] array){\n\
  92         int i=0;\n\
  93         System.out.println( \"*** Printing vector ***\");\n\
  94         for (Object a : array){\n\
  95             i+=1;\n\
  96             System.out.println( \"#\"+i);\n\
  97             System.out.println(a);\n\
  98             System.out.println(  \"*** \"+ i+ \" elements printed! ***\");\n\
  99         }\n\
 100         \r\t}\n")
 101
 102         c.write("public void printModel (Model model) throws Z3Exception{\n\
 103         for (FuncDecl d : model.getFuncDecls()){\n\
 104             System.out.println(d.getName() +\" = \"+ d.toString());\n\
 105               System.out.println(\"\");\n\
 106         }\n\
 107         \r\t}\n")
 108
 109         c.writeln("public int run() throws Z3Exception{")
 110         c.indent()
 111
 112         c.writeln(basename + " p = new " + basename + "();")
 113
 114         #adding time estimation
 115         #c.writeln("int k = 0;")
 116         #c.writeln("long t = 0;")
 117
 118         #c.writeln("for(;k<1;k++){")
 119         #c.indent()
 120
 121         c.writeln("p.resetZ3();")
 122
 123         c.write(os.path.splitext(inputfile)[0] + " model = new " + os.path.splitext(inputfile)[0] + "(p.ctx);\n")
 124
 125         #c.writeln("Calendar cal = Calendar.getInstance();")
 126         #c.writeln("Date start_time = cal.getTime();")
 127
 128         c.write("IsolationResult ret =model.check.checkIsolationProperty(model.")
 129         c.append(source + ", model." + destination + ");\n")
 130         #c.writeln("Calendar cal2 = Calendar.getInstance();")
 131         #c.writeln("t = t+(cal2.getTime().getTime() - start_time.getTime());")
 132
 133         c.writeln("if (ret.result == Status.UNSATISFIABLE){\n\
 134             System.out.println(\"UNSAT\");\n\
 135             return -1;\n\
 136         }else if (ret.result == Status.SATISFIABLE){\n\
 137             System.out.println(\"SAT\");\n\
 138             return 0;\n\
 139         }else{\n\
 140             System.out.println(\"UNKNOWN\");\n\
 141             return -2;\n\
 142         \r\t\t}")
 143
 144         #c.dedent()
 145         #c.writeln("}")
 146
 147         #c.writeln("")
 148         #c.writeln("System.out.printf(\"Mean execution time " + source + " -> " + destination + ": %.16f\", ((float) t/(float)1000)/k);")
 149
 150         c.dedent()
 151         c.writeln("}")
 152
 153         c.dedent()
 154         c.writeln("}")
 155
 156         print >>f, c.end()
 157     logging.debug("File " + os.path.abspath(dirname + "/" + basename + ".java") + " has been successfully generated!!")
 158
 159 if __name__ == "__main__":
 160     main(sys.argv[1:])