001 package escjava.vcGeneration.xml;
002
003 import java.io.File;
004 import java.io.FileInputStream;
005 import java.io.IOException;
006 import java.io.InputStream;
007 import java.io.Writer;
008 import java.util.HashMap;
009 import java.util.Iterator;
010 import java.util.Set;
011
012 import javafe.ast.Expr;
013
014 import javax.xml.parsers.DocumentBuilder;
015 import javax.xml.parsers.DocumentBuilderFactory;
016 import javax.xml.parsers.ParserConfigurationException;
017 import javax.xml.transform.OutputKeys;
018 import javax.xml.transform.Templates;
019 import javax.xml.transform.Transformer;
020 import javax.xml.transform.TransformerConfigurationException;
021 import javax.xml.transform.TransformerException;
022 import javax.xml.transform.TransformerFactory;
023 import javax.xml.transform.dom.DOMSource;
024 import javax.xml.transform.stream.StreamResult;
025 import javax.xml.transform.stream.StreamSource;
026
027 import org.w3c.dom.Attr;
028 import org.w3c.dom.Document;
029 import org.w3c.dom.Element;
030
031 import escjava.translate.GC;
032 import escjava.translate.InitialState;
033 import escjava.vcGeneration.ProverType;
034 import escjava.vcGeneration.TNode;
035 import escjava.vcGeneration.TVisitor;
036 import escjava.vcGeneration.TypeInfo;
037 import escjava.vcGeneration.VariableInfo;
038
039 /**
040 * This class provides a simple mechanism by which new prover plugins to the VC
041 * generator may be implemented.
042 *
043 * <p>All one has to do is to provide a stylesheet within the <i>escjava.vcGeneration.xml</i>
044 * package or located on the system property search path <i>XMLPROVERPATH</i> for the targeted
045 * prover (eg. <i>simplify.xslt</i>). This stylesheet transforms XML terms, conforming to the
046 * DTD defined by <i>escjava/vcGeneration/xml/xmlprover.dtd</i> (as we are compiling with JDK 1.4
047 * this can not be checked!!), into terms of the targeted prover.
048 *
049 * <p>Calling ESC/Java with the nvcg option <i>xml.<prover></i> enables the target prover
050 * VC terms to be generated (eg. <i>-nvcp xml.simplify</i> will enable VC's for the targeted
051 * prover to be generated using the stylesheet <i>escjava/vcGeneration/xml/simplify.xslt</i> -
052 * supplied by default with ESC/Java).
053 *
054 * <p>Using this XML based prover interface should make it easier to build and debug new prover
055 * interfaces to the VC generator.
056 *
057 * @author Carl Pulley
058 */
059 public class XmlProver extends ProverType {
060
061 /**
062 * This field defines the prover based stylesheet that will be used to translate our
063 * generated XML VC terms with calls to {@link XmlProver#getProof}
064 */
065 private String stylesheet = null;
066
067 /**
068 * This method only allows the field {@link XmlProver#stylesheet} to be set <b>once</b>.
069 *
070 * @param stylesheet target prover's stylesheet
071 */
072 public void setStyleSheet(String stylesheet) {
073 if (this.stylesheet == null) {
074 this.stylesheet = stylesheet;
075 }
076 }
077
078 /**
079 * Our DTD specifies that term names are of type CDATA. Hence this method is an identity
080 * renaming. The prover based stylesheet may perform a renaming of these term names.
081 */
082 public String labelRename(String label) {
083 return label;
084 }
085
086 private TXmlVisitor visitor = null;
087
088 public TVisitor visitor(Writer out) throws IOException {
089 if (visitor == null) {
090 visitor = new TXmlVisitor(out);
091 }
092 return visitor;
093 }
094
095 private Document dom = null;
096 private Element node = null;
097
098 /**
099 * Here we ensure that the resulting XML term is suitable for writing to an output file.
100 *
101 * <p>After generating our raw XML term conforming to <i>escjava/vcGeneration/xml/xmlprover.dtd</i>
102 * (this can not be checked with JDK 1.4!!), we convert it to a prover VC term using the stylesheet
103 * specified by {@link XmlProver#stylesheet}.
104 *
105 * <p>The search rules for the stylesheet to be used are as follows (here we assume that <i><stylesheet></i>
106 * is the value of the field {@link XmlProver#stylesheet}):
107 * <ul>
108 * <li>we first look in <i>escjava/vcGeneration/xml</i> for a file named <i><stylesheet>.xslt</i></li>
109 * <li>next we search a :-separated list of directories specified in the system property
110 * <i>XMLPROVERPATH</i> for a file named <i><stylesheet>.xslt</i>. <i>XMLPROVERPATH</i> has a default value of '.'</li>
111 * </ul>
112 */
113 public void getProof(Writer out, String proofName, TNode term) throws IOException {
114 try {
115 DocumentBuilderFactory dbf = DocumentBuilderFactory.newInstance();
116 DocumentBuilder db = dbf.newDocumentBuilder();
117 //FIXME Ideally DTD validation is performed here - but we need JDK 1.5 for that!!
118 dom = db.newDocument();
119 dom.appendChild(dom.createComment("Created by ESC/Java XmlProver"));
120 node = dom.createElement("VCTERM");
121 Attr nameAttr = dom.createAttribute("name");
122 nameAttr.setValue(proofName);
123 node.setAttributeNode(nameAttr);
124 dom.appendChild(node);
125 ((TXmlVisitor) visitor(out)).setDocumentNode(dom, node);
126 generateDeclarations(out, term);
127 generateTerm(out, term);
128 dom.normalize();
129 // Finally, we write our XML data structure to the output stream (transforming it if necessary)
130 TransformerFactory tf = TransformerFactory.newInstance();
131 Transformer tr = null;
132 if (stylesheet == null) {
133 // No stylesheet present, so simply output our XML to the output stream
134 tr = tf.newTransformer();
135 tr.setOutputProperty(OutputKeys.INDENT, "yes");
136 tr.setOutputProperty(OutputKeys.METHOD, "xml");
137 tr.setOutputProperty(
138 "{http://xml.apache.org/xslt}indent-amount", "2");
139 } else {
140 // We have a stylesheet, so transform our XML data and write result as text to the output stream.
141 // Preference is given to stylesheets located within escjava/vcGeneration/xml.
142 // Should the stylesheet not be found in that location, then directories specificed within the
143 // system property XMLPROVERPATH are searched.
144 // If XMLPROVERPATH is not defined, then it defaults to the current working directory (ie. the
145 // directory within which ESC/Java has been invoked).
146 InputStream src = getClass().getResourceAsStream(stylesheet + ".xslt");
147 if (src == null) {
148 // The stylesheet is not located within the jar file at escjava/vcGeneration/xml, so we
149 // first read in the XMLPROVERPATH system property. If this is not defined, then we
150 // provide a default value of '.'
151 File fileSrc = null;
152 String xmlproverpath = System.getProperty("XMLPROVERPATH",
153 ".");
154 // The following code guards against XMLPROVERPATH being defined as an empty string
155 if (xmlproverpath.equals("")) {
156 xmlproverpath = ".";
157 }
158 // Directories within the system property XMLPROVERPATH are now searched in order to
159 // locate the stylesheet.
160 String[] path = xmlproverpath.split(":");
161 for (int index = 0; index < path.length; index++) {
162 fileSrc = new File(path[index] + "/" + stylesheet
163 + ".xslt");
164 if (fileSrc.exists() && fileSrc.isFile()
165 && fileSrc.canRead()) {
166 src = new FileInputStream(fileSrc);
167 break;
168 }
169 }
170 if (src == null) {
171 // We didn't find a stylesheet within the XMLPROVERPATH directories, so register an error by raising an exception
172 throw new XmlProverException(stylesheet);
173 } else {
174 System.out.println("[XmlProver: using "
175 + fileSrc.toString() + "]");
176 }
177 } else {
178 System.out
179 .println("[XmlProver: using escjava/vcGeneration/xml/"
180 + stylesheet + ".xslt]");
181 }
182 Templates transformation = tf
183 .newTemplates(new StreamSource(src));
184 tr = transformation.newTransformer();
185 //tr.setOutputProperty(OutputKeys.METHOD, "text");
186 //tr.setOutputProperty(OutputKeys.STANDALONE, "yes");
187 //tr.setOutputProperty(OutputKeys.OMIT_XML_DECLARATION, "yes");
188 }
189 tr.transform(new DOMSource(dom), new StreamResult(out));
190 } catch (TransformerConfigurationException exn) {
191 System.out.println("XmlProver: " + exn);
192 } catch (TransformerException exn) {
193 System.out.println("XmlProver: " + exn);
194 } catch (ParserConfigurationException exn) {
195 System.out.println("XmlProver: " + exn);
196 }
197 }
198
199 /**
200 * Since our XML mapping of variable names is the identity one, we may simply
201 * return the old variable name here.
202 */
203 public String getVariableInfo(VariableInfo caller) {
204 return caller.old;
205 }
206
207 /**
208 * Since our XML mapping of type names is the identity one, we may simply
209 * return the old type name here.
210 */
211 public String getTypeInfo(TypeInfo caller) {
212 return caller.old;
213 }
214
215 /**
216 * Initialization simply defines an identity map on the known types and names.
217 */
218 public void init() {
219 // Predefined types
220 TNode._Reference = TNode.addType("%Reference", "%Reference");
221 TNode._Time = TNode.addType("%Time", "%Time");
222 TNode._Type = TNode.addType("%Type", "%Type");
223 TNode._boolean = TNode.addType("boolean", "boolean");
224 TNode._char = TNode.addType("char", "char");
225 TNode._DOUBLETYPE = TNode.addType("DOUBLETYPE", "DOUBLETYPE");
226 TNode._double = TNode.addType("double", "double");
227 TNode._Field = TNode.addType("%Field", "%Field");
228 TNode._INTTYPE = TNode.addType("INTTYPE", "INTTYPE");
229 TNode._integer = TNode.addType("integer", "integer");
230 TNode._float = TNode.addType("float", "float");
231 TNode._Path = TNode.addType("%Path", "%Path");
232 //TNode._String = addType("String", "String"); FIXME, does this type appears in original proof ?
233
234 // Predefined variables name
235 // variables used by the old proof system and that we still need
236 TNode.addName("ecReturn", "%Path", "ecReturn");
237 TNode.addName("ecThrow", "%Path", "ecThrow");
238 TNode.addName("XRES", "%Reference", "XRES");
239 }
240
241 /**
242 * At this stage, we do not know if the target prover is typed or not. Hence, we add the typing
243 * predicate to the VC term. The prover based stylesheet may eliminate this typing predicate.
244 */
245 public Expr addTypeInfo(InitialState initState, Expr tree) {
246 tree = GC.implies(initState.getInitialState(), tree);
247 return tree;
248 }
249
250 /**
251 * All rewriting is handled by the prover based stylesheet, so we do nothing here.
252 */
253 public TNode rewrite(TNode tree) {
254 return tree;
255 }
256
257 public void generateDeclarations(/*@non_null*/Writer s, HashMap variableNames) throws IOException {
258 Set keySet = variableNames.keySet();
259 Iterator iter = keySet.iterator();
260 String keyTemp = null;
261
262 while (iter.hasNext()) {
263 keyTemp = (String) iter.next();
264 VariableInfo viTemp = (VariableInfo) variableNames.get(keyTemp);
265 Element decln = dom.createElement("DECLN");
266 if (viTemp != null) {
267 Attr nameAttr = dom.createAttribute("name");
268 nameAttr.setValue(viTemp.getVariableInfo());
269 decln.setAttributeNode(nameAttr);
270 if (viTemp.type != null) {
271 Attr typeAttr = dom.createAttribute("type");
272 typeAttr.setValue(viTemp.type.getTypeInfo());
273 decln.setAttributeNode(typeAttr);
274 }
275 }
276 node.appendChild(decln);
277 }
278 }
279
280 }