#/usr/bin/python
import os
import re

basic_path = "/scratch/vsahil/klee/singapore/exten_version3/"
file_now = "sat-aim100_klee/"
path = basic_path+file_now

files_directory = os.listdir(path)
for i in files_directory:
	if "klee-out" in i: # this are the klee-out files
		infile = open(path+i+"/info",'r')
		infile_sec = open(path+i+"/messages.txt","r")
		file_here = infile.read().splitlines()
		messages = infile_sec.read().splitlines()
		kill = False
		for m in messages:
			if "invalid klee_assume call (provably false)" in m:
				kill = True		# don't take such a file, as it is UNSAT. This is only for intensional constraints, for extensional things will be different, generally it doesn't have klee_assume calls, so it might work there as well
		infile.close()
		infile_sec.close()
		if(kill):
			continue   # see where kill is assigned true
		xml_name = file_here[0].split()[-1][:-2]+"xml"  # this gives me the xml file names for that directory, [:-2] for removing .bc from the files
		infile = open(basic_path+"../constraints/"+file_now[:-6]+"/"+xml_name, 'r')		# this only works for files with names ending with "_c", because llbmc gives no error
		xml = infile.read().splitlines()
		infile.close()
		print xml_name, i 
		c_here = file_here[0].split()[-1][:-2]+"c"
		infile = open(path+c_here, 'r')
		var = infile.read().splitlines()  # Read the contents of the file.
		infile.close()
		
		# now for finding the file which is to be verified, that is the file which ends with ".err"
		test_directory = os.listdir(path+i)
		verify_files = []
		values = []
		for j in test_directory:
			if ".err"  in j:
  				verify_files.append(j)
  		if(len(verify_files) == 0):
			continue
		for j, k in enumerate(verify_files):
  			verify_files[j] = re.findall(r"[\w']+", verify_files[j])[0]+".ktest"
  			# print verify_files			# now this array has all the files that need to be verified for this xml file, # now i need to run ktest tool on each of them, direct output to a file, add that to xml and done
  			os.system("ktest-tool --write-ints " + path + i + "/" + verify_files[j] + " > temp.txt")		# so now the file is in temp.txt
  			infile = open('temp.txt', 'r')  # Open the file for reading.
			values = infile.read().splitlines()  # Read the contents of the file.
			infile.close()


		# infile = open('CryptoPuzzle-black-green-orange.xml', 'r')  # Open the file for reading.
		# xml = infile.read().splitlines()  # Read the contents of the file.
		# infile.close()

		# infile = open('CryptoPuzzle-black-green-orange.c', 'r')  # Open the file for reading.
		# var = infile.read().splitlines()  # Read the contents of the file.
		# infile.close()

		# infile = open('temp.txt', 'r')  # Open the file for reading.
		# values = infile.read().splitlines()  # Read the contents of the file.
		# infile.close()

		# this part below reads the txt file generated by ktest tool and adds that to xml file as part of intensional constraint


		dictionary = {}

		for i, j in enumerate(var):
			if "/*" in j:
				i +=1  # to skip the "/* line"
				while not "*/" in var[i]:
					s = var[i].split()	# splits on space
					# print int(s[0]), s[1]   # now s[1] is the variable, and s[0] will be its sequence no. like var0, var29
					dictionary[int(s[0])] = s[1]		# add it in the dictionary	
					i+=1
				break		# now no need to go ahead

		# print dictionary	# now i have the dictionary with all the variables and its corresponding sequence no.


		# print values
		br = 0
		for i, j in enumerate(values):
			if "num objects" in j: 		# the next line is where objects are going to start
				br = i + 1			# br has the value stored for the array index for 
				break

		dict2 = {}

		for i in range(br, len(values), 3):		# for the next element
			name = values[i].split()[-1]	# the last element
			val = values[i+2].split()[-1]	# again the last element
			i = name.index('r')			# the name is like 'var89', so start from after letter 'r' upto second last element
			name = int(name[i+1:-1])
			# print "name: ", name, " val: ", int(val)
			dict2[name] = int(val)

		# print dict2			# now dict2 has the variables with the name as in dictionary but with its values
							# now we can print this into xml file, names with corresponding values


		# I will add the constraints of each variable value before the closing constraint tag.
		
		write_file = open(path+xml_name, "w")	# this creates a xml file in the C directory, all these xml files must be SATISFIABLE, because they have been created only because they had were SAT in first place and this is verifing whether the solution given by KLEE is indeed a solution to XML file or not

		for i, j in enumerate(xml):
			if not "/constraints" in j:  
				# print j
				write_file.write(j)
				write_file.write("\n")
			else:		# this is the end of constraints, we will add all the values here	
				# print "	<group>"
				write_file.write("    <group>\n")
				# print "		<intension> eq(%0,%1) </intension>"			# maintain proper format
				write_file.write("	    <intension> eq(%0,%1) </intension>\n")
				for k in dict2.keys():
					# print " 		<args>", dictionary[k], dict2[k], "</args>"
					write_file.write(" 	    <args> ")
					write_file.write(str(dictionary[k])+" ")  # This space was so necessary, without this inexplicable error was occuring
					write_file.write(str(dict2[k]))
					write_file.write(" </args>\n")
				# print "	</group>"
				write_file.write("    </group>\n")
				# print "  </constraints>"
				write_file.write("  </constraints>\n")
		write_file.close()
