    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    }