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[ ]*:([^;]*);')

re_frama_res = re.compile('Proved goals:[ ]*([0-9]*)[ ]*/[ ]*([0-9]*)')

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", "KEEP")

	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", "10", "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)

	answer = root.find(".//Answer")

	if answer is None:

		return (None, "NO_ANS", None)

	if answer.text != "valid":

		return (None, "INVALID", None)

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

	if k is None:

		return (None, "NO_K", 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)+")", "KEEP")

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), None)

	return (lines, "OK", None)

def framac(lines, temp):

	FRAMAC=["frama-c", temp+"/top.c"]

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

	(stdout, stderr) = p.communicate()

	res = p.wait()

	if res != 0:

		return (None, "PARSE_"+str(res), None)

	FRAMAC=["frama-c", "-wp", "-wp-prover", "CVC4,alt-ergo,z3,coq", temp+"/top.c", "-wp-par", "2", "-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"]

	#"-wp-rte", 

	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), None)

	m = re_frama_res.search(stdout)

	if not m:

		return (None, "BAD_OUT", None)

	return (lines, str(m.group(1))+"/"+str(m.group(2)), None)

def parseFile(inp, todo):

	lines = inp.readlines()

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

	res = ""

	data = None

	ok = False

	for f in todo:

		x = [[]]

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

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

		if newlines:

			lines = newlines

		if cmd == "STOP":

			break

		if cmd == "KEEP":

			ok = True

	if ok:

		res += "WRITE"

		data = "".join(lines)

	shutil.rmtree(temp)

	return (res, data)

TODO=[modProperties, addEnsures, addK, compileLustre, framac]

LENGTH=40

target="./generated/"

#if os.path.exists(target):

#	shutil.rmtree(target)

orig = "./tests/"

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")

		(res, data) = parseFile(inp, TODO)

		inp.close()

		if data:

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

			out.write(data)

			out.close()

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

		sys.stdout.flush()