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 }