CristalCaveGem » LustreC

import sys

import os

import re

import tempfile

import subprocess

import shutil

import xml.etree.ElementTree as ET

re_property_old = re.compile('--%[ ]*PROPERTY([^;]*);')

re_property = re.compile('--![ ]*PROPERTY[ ]*:([^;]*);')

re_node = re.compile('.*node.*')

re_ensures = re.compile('.*ensures.*')

re_k = re.compile('--![ ]*k[ ]*:([^;]*);')

def findInLines(lines, regex):

	res = []

	for i in range(len(lines)):

		m = regex.search(lines[i])

		if m:

			res.append((i, m.groups()[0] if len(m.groups()) > 0 else None))

	return res

def modProperties(lines, temp):

	properties_old = findInLines(lines, re_property_old)

	if not properties_old:

		return (None, "NO_OLD", None)

	for (i, data) in properties_old:

		lines[i] = "--!PROPERTY:{};\n".format(data)

	return (lines, "OK", None)

def addEnsures(lines, temp):

	nodes = findInLines(lines, re_node)

	ensures = findInLines(lines, re_ensures)

	properties = findInLines(lines, re_property)

	if not nodes:

		return (None, "NONODE", None)

	if ensures:

		return (None, "ALREADY", None)

	if not properties:

		return (None, "NOPR", None)

	if len(properties) > 1:

		return (None, "TOOMUCHPR", None)

	for (i, data) in properties:

		bestd = len(lines)

		best = -1

		for (j, _) in nodes:

			if i - j < bestd:

				bestd = i - j

				best = j

		lines.insert(best, "--@ensures " + data + ";\n")

	return (lines, "OK", None)

TIMEOUT=1

MAX=10

def addK(lines, temp):

	properties = findInLines(lines, re_property)

	k = findInLines(lines, re_k)

	if k:

		return (None, "ALREADY", None)

	if not properties:

		return (None, "NOPR", None)

	if len(properties) > 1:

		return (None, "TOOMUCHPR", None)

	top = temp + "/no_k.lus"

	f = open(top, 'w')

	f.write("".join(lines))

	f.close()

	p = subprocess.Popen(["timeout", "40", "pkind", top, "-timeout", str(TIMEOUT), "-k_incremental", str(MAX)], stdout=subprocess.PIPE, stderr=subprocess.PIPE)

	(stdout, stderr) = p.communicate()

	try:

		root = ET.fromstring(stdout)

	except ET.ParseError:

		return (None, "TIMEOUT", None)

	k = root.find(".//K")

	if k is None:

		return (None, "ERR", None)

	try:

		k = int(k.text)

	except ValueError:

		return (None, "NOTPROVED", None)

	lines.insert(properties[0][0], "--!k:{};\n".format(k))

	return (lines, "OK("+"k=" + str(k)+")", None)

def compileLustre(lines, temp):

	top = temp + "/top.lus"

	f = open(top, 'w')

	f.write("".join(lines))

	f.close()

	p = subprocess.Popen(["lustrec", "-d", temp ,"-acsl-proof",  top], stdout=subprocess.PIPE, stderr=subprocess.PIPE)

	(stdout, stderr) = p.communicate()

	res = p.wait()

	if res != 0:

		return (None, "ERR_"+str(res), stdout+"\n-------\n"+stderr)

	return (lines, "OK", None)

def framac(lines, temp):

	FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-wp-rte", "-wp-model", "ref", """-wp-tactic="Require Why3. intros. hnf. repeat split;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10""", "-wp-script", temp+"/top.coq" "-wp-no-let"]

	p = subprocess.Popen(FRAMAC, stdout=subprocess.PIPE, stderr=subprocess.PIPE)

	(stdout, stderr) = p.communicate()

	res = p.wait()

	if res != 0:

		return (None, "ERR_"+str(res), temp+"\n"+stdout+"\n-------\n"+stderr)

	return (lines, "OK", stdout)

def parseFile(inp, out, todo):

	lines = inp.readlines()

	temp = tempfile.mkdtemp(prefix="contracts_")

	res = ""

	dats = []

	for f in todo:

		x = [[]]

		(newlines, r, data) = f(lines[:], temp)

		res += "{:10} ".format(r[:10])

		if newlines:

			lines = newlines

		if data:

			dats.append(data)

	out.write("".join(lines))

	shutil.rmtree(temp)

	return (res, dats)

TODO=[modProperties, addEnsures, addK, compileLustre]

LENGTH=50

target="./generated/"

#if os.path.exists(target):

#	shutil.rmtree(target)

orig = "/home/davyg/good"

for root, dirs, files in os.walk(orig):

	short = root[len(orig):]

	os.mkdir(target+"/"+short)

	for x in files:

		if not x.endswith(".lus"):

			continue

		inp = open(root+"/"+x, "r")

		out = open(target+"/"+short+"/"+x, "w")

		(res, dats) = parseFile(inp, out, TODO)

		inp.close()

		out.close()

		print(("Process {0:"+str(LENGTH)+"} : {1}").format(("./"+short+"/"+x)[:LENGTH], res))

		if dats:

			print("\n/////////////////////\n".join(dats))

		sys.stdout.flush()