001 package escjava.vcGeneration.pvs;
002
003 import java.util.HashMap;
004 import java.util.Iterator;
005 import java.util.Set;
006 import java.util.regex.Matcher;
007 import java.util.regex.Pattern;
008 import java.io.*;
009
010 import javafe.ast.Expr;
011
012 import escjava.translate.InitialState;
013 import escjava.vcGeneration.*;
014
015 public class PvsProver extends ProverType {
016
017 public String labelRename(String label) {
018 label = label.replace('.','_');
019 return label;
020 }
021
022 public TVisitor visitor(Writer out) throws IOException {
023 return new TPvsVisitor(out);
024 }
025
026 public void getProof(Writer out, String proofName, TNode term) throws IOException {
027 try {
028 out.write(proofName + " : CONJECTURE\n"); // let's be modest...
029 out.write("ForAll(\n");
030 generateDeclarations(out, term);
031 out.write(") :\n\n");
032 generateTerm(out, term);
033 } catch (IOException e) {
034 // Intentionally do nothing
035 }
036 }
037
038 public String getVariableInfo(VariableInfo caller) {
039
040 if (caller.type != TNode._Type) {
041 if (caller.def == null)
042 pvsRename(caller);
043
044 return caller.def;
045 } else {
046 /*
047
048 When variable is a type, we first have to check if it's in the type table.
049 If yes, we take the name here (it's the case with predefined types like INTYPE, integer, Reference etc...
050
051 Else it's normally a user defined Type
052
053 */
054
055 Set keySet = TNode.typesName.keySet();
056 Iterator iter = keySet.iterator();
057 TypeInfo tiTemp = null;
058 String keyTemp = null;
059
060 while (iter.hasNext()) {
061
062 try {
063 keyTemp = (String) iter.next();
064 } catch (Exception e) {
065 System.err.println(e.getMessage());
066 }
067 tiTemp = (TypeInfo) TNode.typesName.get(keyTemp);
068
069 if (tiTemp.old.equals(caller.old)) {
070 return getTypeInfo(tiTemp);
071 }
072
073 }
074
075 TDisplay
076 .warn(
077 this,
078 "getTypeInfo()",
079 "Considering "
080 + caller.old
081 + " as a user defined type, or a not (yet) handled variable.");
082
083 pvsRename(caller);
084
085 return caller.def;
086 }
087
088 }
089
090 /* @
091 @ ensures pvs != null;
092 @ */
093 private void pvsRename(VariableInfo caller) {
094
095 // definitions of different regexp used.
096 Pattern p1 = Pattern.compile("\\|(.*):(.*)\\.(.*)\\|");
097 Matcher m1 = p1.matcher(caller.old);
098
099 // <variables not handled>
100 Pattern p2 = Pattern.compile("Unknown tag <.*>");
101 Matcher m2 = p2.matcher(caller.old);
102
103 Pattern p3 = Pattern.compile("\\|brokenObj<.*>\\|");
104 Matcher m3 = p3.matcher(caller.old);
105 // </variables not handled>
106
107 String name = null;
108 String line = null;
109 String column = null;
110
111 int i = 0;
112
113 //System.out.println("Performing regular expression matching against "+old+" ");
114
115 /*
116 This case is done first because some variables not handled are "%Type" ones
117 and thus otherwise they will be matched by the next if construct
118 */
119 if (m2.matches() || m3.matches() || caller.old.equals("brokenObj")) { // variable is not handled yet, ask David Cok about
120 // some things
121 caller.def = "%NotHandled";
122 }
123
124 // <case 1>
125 /*
126 If variable's a type, we must prefix his renaming by userDef?.
127 Why ?
128 Because if the user defined a type named 'Reference', otherwise we will use is as it
129 in the proof and it will interfer with our predefined types.
130
131 Since '?' isn't a valid character in the java notation and is Ok for pvs,
132 we use it to make the difference.
133 */
134 else if (caller.type == TNode._Type) {
135 TDisplay.warn(this, "pvsRename()", "Considering " + caller.old
136 + " as a user defined type.");
137
138 // renaming done here
139 caller.def = "userDef?" + caller.old;
140 }
141 // </case 1>
142
143 // <case 2>, capturing |y:8.31|
144 else if (m1.matches()) {
145 //@ assert m1.groupCount() == 3;
146
147 if (m1.groupCount() != 3)
148 TDisplay.err(this, "pvsRename()", "m.groupCount() != 3");
149
150 for (i = 1; i <= m1.groupCount(); i++) {
151
152 if (m1.start(i) == -1 || m1.end(i) == -1)
153 TDisplay.err(this, "pvsRename()",
154 "Return value of regex matching is -1");
155 else {
156
157 String temp = caller.old.substring(m1.start(i), m1.end(i));
158 //@ assert temp != null;
159
160 switch (i) {
161 case 1:
162 name = temp;
163 //@ assert name != null;
164 break;
165 case 2:
166 line = temp;
167 //@ assert line != null;
168 break;
169 case 3:
170 column = temp;
171 //@ assert column != null;
172 break;
173 default:
174 TDisplay.err(this, "pvsRename()",
175 "Switch call incorrect, switch on value " + i);
176 break;
177 }
178 } // no error in group
179
180 } // checking all group
181
182 /* renaming done here, if you want the way it's done
183 (for pattern like |y:8.31|)
184 do it here. */
185 caller.def = name + "_" + line + "_" + column;
186
187 } // </case 2>
188 else {
189 caller.def = caller.old; // FIXME handle everything
190 } // regexp didn't match
191 }
192
193 public String getTypeInfo(TypeInfo caller) {
194 if (caller.def == null)
195 pvsRename(caller);
196 return caller.def;
197 }
198
199 /* @
200 @ ensures pvs != null;
201 @ */
202 private void pvsRename(TypeInfo caller) {
203
204 if (caller.old.equals("null"))
205 caller.def = "Reference";
206 else {
207 // common rules here //fixme, be more specific maybe
208 if (caller.old.startsWith("java.")) //check if in the form java.x.y
209 caller.def = caller.old.replace('.', '_');
210 else {
211 TDisplay.warn(this, "pvsRename()", "Type not handled : "
212 + caller.old);
213 TDisplay
214 .warn(this, "pvsRename()",
215 "Considering it as a user defined type... ie ReferenceType");
216 caller.def = "ReferenceType";
217 }
218 }
219 }
220
221 public void init() {
222 // Predefined types
223
224 TNode._Reference = TNode.addType("%Reference", "Reference");
225 TNode._Time = TNode.addType("%Time", "Time");
226 TNode._Type = TNode.addType("%Type", "ReferenceType");
227 TNode._boolean = TNode.addType("boolean", "Boolean");
228 TNode._char = TNode.addType("char", "T_char");
229 TNode._DOUBLETYPE = TNode.addType("DOUBLETYPE", "ContinuousNumber"); // fixme, is it JavaNumber or BaseType ?
230 TNode._double = TNode.addType("double", "ContinuousNumber"); //fixme
231 TNode._Field = TNode.addType("%Field", "Field"); // fixme there's a lot of different fields in the pvs logic, I need to capture that
232 TNode._INTTYPE = TNode.addType("INTTYPE", "T_int"); //fixme like DOUBLETYPE
233 TNode._integer = TNode.addType("integer", "DiscreteNumber"); //fixme
234 TNode._float = TNode.addType("float", "ContinuousNumber");
235 TNode._Path = TNode.addType("%Path", "Path"); // used to modelize different ways
236 // of terminating a function
237 //_String = addType("String" "String"); fixme, does this type appears in original proof ?
238
239 // Predefined variables name
240 // variables used by the old proof system and that we still need
241 TNode.addName("ecReturn", "%Path", "preDef?ecReturn");
242 TNode.addName("ecThrow", "%Path", "preDef?ecThrow");
243 TNode.addName("XRES", "%Reference", "preDef?XRes");
244 }
245
246 public Expr addTypeInfo(InitialState initState, Expr tree) {
247 return tree;
248 }
249
250 /** We expect this method to be called with a tree of type TBoolImplies:
251 * <ul>
252 * <li>the hypothesis of the tree is expected to be typing information</li>
253 * <li>the conclusion of the tree is expected to be the VC body</li>
254 * </ul>
255 * Since the Pvs prover is a strongly typed logic, we may eliminate this typing
256 * information <i>before</i> providing any additional simplifications.
257 *
258 * Strictly speaking, we should check that the hypothesis is as expected (FIXME).
259 */
260 public TNode rewrite(TNode tree) {
261 TProofSimplifier psvi = new TProofSimplifier();
262 try {
263 tree.accept(psvi);
264 } catch (IOException e) {
265 // This should never happen!
266 System.out.println(e.getMessage());
267 }
268 return tree;
269 }
270
271 public void generateDeclarations(/*@ non_null */ Writer s, HashMap variablesName) throws IOException {
272 Set keySet = variablesName.keySet();
273
274 Iterator iter = keySet.iterator();
275 String keyTemp = null;
276 VariableInfo viTemp = null;
277
278 /*
279 * Needed to avoid adding a comma after last declaration. As some declaration can be skipped
280 * it's easier to put comma before adding variable (thus need for testing firstDeclaration
281 * instead of last one)
282 */
283 boolean firstDeclarationDone = false;
284
285 while (iter.hasNext()) {
286
287 try {
288 keyTemp = (String) iter.next();
289 } catch (Exception e) {
290 System.err.println(e.getMessage());
291 }
292 viTemp = (VariableInfo) variablesName.get(keyTemp);
293
294 /* output informations in this format : oldName, pvsUnsortedName,
295 * pvsName, sammyName, type.
296 */
297 if (viTemp.type != null) {
298 try {
299 if (firstDeclarationDone
300 && !viTemp.getVariableInfo().equals("%NotHandled"))
301 s.write(",\n");
302
303 if (!viTemp.getVariableInfo().equals("%NotHandled")) { // skipping non handled variables
304 s.write(viTemp.getVariableInfo() + " : "
305 + viTemp.type.getTypeInfo());
306
307 if (!firstDeclarationDone)
308 firstDeclarationDone = true;
309 }
310 } catch (IOException e) {
311 // Intentionally do nothing
312 }
313 } else
314 // FIXME test that it nevers happen
315 TDisplay
316 .warn(
317 this,
318 "generateDeclarations",
319 "Type of variable "
320 + keyTemp
321 + " is not set when declarating variables for the proof, skipping it...");
322 }
323 }
324 }