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    
036      //@ ensures isStarted && prover != null;
037      synchronized
038      static public void start() {
039        
040        if (isStarted) return;
041        
042        if( useSammy && (sammy == null || !sammy.started) ){
043          long startTimeSammy = java.lang.System.currentTimeMillis();
044          
045          System.out.println("Launching demo of sammy...");
046          
047          Sammy.main(new String[0]);
048          
049          System.out.println("exiting...");
050          System.exit(0);
051          
052        }
053        
054        if( useSimplify && (simplify == null)) { 
055          
056          long startTime = java.lang.System.currentTimeMillis();
057          simplify = new Simplify();
058          
059          if (!Main.options().quiet)
060            System.out.println("  Prover started:" + Main.timeUsed(startTime));
061          
062          escjava.backpred.BackPred.genUnivBackPred(simplify.subProcessToStream());
063          simplify.sendCommands("");
064          
065        }
066        
067        if (listener != null) listener.stateChanged(1);
068        isStarted = true;
069        status = STARTED;
070        
071      }
072      
073      synchronized
074      static public Simplify prover() {
075        start();
076        return simplify;
077      }
078      
079      //@ ensures status == NOTSTARTED && prover == null;
080      synchronized
081      static public void kill() {
082        
083        if(useSimplify) {
084          if (simplify != null) 
085            simplify.close();
086          
087          simplify = null;
088        }
089        
090        if(useSammy) {
091          sammy.stop_prover();
092          sammy = null;
093        }
094        
095        if (listener != null) 
096          listener.stateChanged(0);
097        
098        isStarted = false;
099        status = NOTSTARTED;
100      }
101      
102      synchronized
103      static public void died() {
104        
105        if(useSimplify) {
106          if (simplify != null) 
107            simplify.close();
108          
109          simplify = null;
110        }
111        
112        if(useSammy) {
113          sammy.stop_prover();
114          sammy = null;
115        }
116        
117        if (listener != null) 
118          listener.stateChanged(0);
119        
120        isStarted = false;
121        status = NOTSTARTED;
122      }
123      
124      /*
125       * Specific to simplify
126       */
127      synchronized
128      static public void push(/*@ non_null @*/ Expr vc) {
129        PrintStream ps = simplify.subProcessToStream();
130        ps.print("\n(BG_PUSH ");
131        VcToString.computePC(vc, ps);
132        ps.println(")");
133        simplify.sendCommands("");
134      }
135      
136      synchronized
137      static public void push(FindContributors scope) {
138        start();
139        if (simplify != null) {
140          PrintStream ps = simplify.subProcessToStream();
141          ps.print("\n(BG_PUSH ");
142          escjava.backpred.BackPred.genTypeBackPred(scope, ps);
143          ps.println(")");
144          simplify.sendCommands("");
145          savedScope = scope;
146          status = PUSHED;
147        }
148      }
149      
150      //@ requires vc != null;
151      // scope can be null
152      //? ensures \result != null;
153      synchronized
154      static public Enumeration prove(Expr vc, FindContributors scope) {
155        
156        if (scope == null) {
157          if (savedScope != null && status != PUSHED) push(savedScope);
158        } else {
159          if (status == PUSHED) {
160            if (savedScope != scope) {
161              pop();
162              push(scope);
163            }
164          } else {
165            push(scope);
166          }
167        }
168        if (listener != null) listener.stateChanged(2);
169        try {
170          simplify.startProve();
171          VcToString.compute(vc, simplify.subProcessToStream());
172     
173          Enumeration en = simplify.streamProve();
174          if (listener != null) listener.stateChanged(1);
175          return en;
176        } catch (FatalError e) {
177          died();
178          return null;
179        }
180      }
181      
182      /*
183       * Specific to simplify
184       */
185      synchronized
186      static public void pop() {
187        if (simplify != null)
188          simplify.sendCommand("(BG_POP)");
189        savedScope = null;
190        status = STARTED;
191      }
192      
193      /**
194       * Our Simplify instance.
195       */
196      //-@ monitored
197      public static Simplify simplify;
198      //@ private invariant isStarted ==> prover != null;
199      
200      /*
201       * Our Sammy instance \\o \o/ o//
202       */
203      public static Sammy sammy;
204      //@ public static model Object prover;
205      //@ static represents prover <- sammy;
206      
207    }