001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava;
004
005 import escjava.backpred.FindContributors;
006 import escjava.prover.*;
007 import escjava.translate.VcToString;
008 import javafe.ast.ASTNode;
009 import javafe.ast.Expr;
010 import javafe.util.FatalError;
011 import java.io.PrintStream;
012 import java.util.Enumeration;
013 import java.util.Properties;
014
015 public class ProverManager {
016
017 public static interface Listener {
018 void stateChanged(int s);
019 }
020 public static Listener listener = null;
021
022 final static private int NOTSTARTED = 0;
023 final static private int STARTED = 1;
024 final static private int PUSHED = 2;
025
026 /*@ spec_public */ static private int status = 0;
027 /*@ spec_public */ static private boolean isStarted = false;
028 //@ private invariant status != NOTSTARTED <==> isStarted;
029
030 static private FindContributors savedScope = null;
031
032 public static boolean useSimplify = false;
033 public static boolean useSammy = false;
034 public static boolean useHarvey = false;
035 public static boolean useCvc3 = false;
036
037 //@ ensures isStarted && prover != null;
038 synchronized
039 static public void start() {
040
041 if (isStarted) return;
042
043 if( useSammy && (sammy == null || !sammy.started) ){
044 long startTimeSammy = java.lang.System.currentTimeMillis();
045
046 System.out.println("Launching demo of sammy...");
047
048 Sammy.main(new String[0]);
049
050 System.out.println("exiting...");
051 System.exit(0);
052
053 }
054
055 if( useSimplify && (simplify == null)) {
056
057 long startTime = java.lang.System.currentTimeMillis();
058 simplify = new Simplify();
059
060 if (!Main.options().quiet)
061 System.out.println(" Prover started:" + Main.timeUsed(startTime));
062
063 escjava.backpred.BackPred.genUnivBackPred(simplify.subProcessToStream());
064 simplify.sendCommands("");
065
066 }
067
068 if (useCvc3 && (cvc3 == null || !cvc3.started)) {
069 long startTime = java.lang.System.currentTimeMillis();
070 if (cvc3 == null)
071 cvc3 = new Cvc3(true);
072
073 if (!Main.options().quiet)
074 System.out.println(" Prover started:" + Main.timeUsed(startTime));
075
076 // set any flags here (-tcc and timeout, for example)
077 Properties flags = new Properties();
078 flags.setProperty(" ","-timeout 0");
079 cvc3.set_prover_resource_flags(flags);
080
081 cvc3.start_prover();
082 // note: the backpred is included as part of the vcGen code
083 }
084
085 if (listener != null) listener.stateChanged(1);
086 isStarted = true;
087 status = STARTED;
088
089 }
090
091 synchronized
092 static public Simplify prover() {
093 start();
094 return simplify;
095 }
096
097 //@ ensures status == NOTSTARTED && prover == null;
098 synchronized
099 static public void kill() {
100
101 if(useSimplify) {
102 if (simplify != null)
103 simplify.close();
104
105 simplify = null;
106 }
107
108 if(useSammy) {
109 sammy.stop_prover();
110 sammy = null;
111 }
112
113 if(useCvc3) {
114 cvc3.stop_prover();
115 cvc3 = null;
116 }
117
118 if (listener != null)
119 listener.stateChanged(0);
120
121 isStarted = false;
122 status = NOTSTARTED;
123 }
124
125 synchronized
126 static public void died() {
127
128 if(useSimplify) {
129 if (simplify != null)
130 simplify.close();
131
132 simplify = null;
133 }
134
135 if(useSammy) {
136 sammy.stop_prover();
137 sammy = null;
138 }
139
140 if (listener != null)
141 listener.stateChanged(0);
142
143 if(useCvc3) {
144 cvc3.stop_prover();
145 cvc3 = null;
146 }
147
148 isStarted = false;
149 status = NOTSTARTED;
150 }
151
152 /*
153 * Specific to simplify
154 */
155 synchronized
156 static public void push(/*@ non_null @*/ Expr vc) {
157 PrintStream ps = simplify.subProcessToStream();
158 ps.print("\n(BG_PUSH ");
159 VcToString.computePC(vc, ps);
160 ps.println(")");
161 simplify.sendCommands("");
162 }
163
164 synchronized
165 static public void push(FindContributors scope) {
166 start();
167 if (simplify != null) {
168 PrintStream ps = simplify.subProcessToStream();
169 ps.print("\n(BG_PUSH ");
170 escjava.backpred.BackPred.genTypeBackPred(scope, ps);
171 ps.println(")");
172 simplify.sendCommands("");
173 savedScope = scope;
174 status = PUSHED;
175 }
176 }
177
178 //@ requires vc != null;
179 // scope can be null
180 //? ensures \result != null;
181 synchronized
182 static public Enumeration prove(Expr vc, FindContributors scope) {
183
184 if (useSimplify) {
185 if (scope == null) {
186 if (savedScope != null && status != PUSHED) push(savedScope);
187 } else {
188 if (status == PUSHED) {
189 if (savedScope != scope) {
190 pop();
191 push(scope);
192 }
193 } else {
194 push(scope);
195 }
196 }
197 if (listener != null) listener.stateChanged(2);
198 try {
199 simplify.startProve();
200 VcToString.compute(vc, simplify.subProcessToStream());
201
202 Enumeration en = simplify.streamProve();
203 if (listener != null) listener.stateChanged(1);
204 return en;
205 } catch (FatalError e) {
206 died();
207 return null;
208 }
209 }
210 else {
211 return null;
212 }
213 }
214
215 /*
216 * Specific to simplify
217 */
218 synchronized
219 static public void pop() {
220 if (simplify != null)
221 simplify.sendCommand("(BG_POP)");
222 savedScope = null;
223 status = STARTED;
224 }
225
226 /**
227 * Our Simplify instance.
228 */
229 //-@ monitored
230 public static Simplify simplify;
231 //@ private invariant isStarted ==> prover != null;
232
233 /*
234 * Our Sammy instance \\o \o/ o//
235 */
236 public static Sammy sammy;
237 //@ public static model Object prover;
238 //@ static represents prover <- sammy;
239
240 /*
241 * Our Cvc3 instance.
242 */
243 public static Cvc3 cvc3;
244 }