|
166 | 166 | (egglog-program-add! `(run-schedule (repeat 1 run-extract-commands)) curr-program) |
167 | 167 |
|
168 | 168 | ;;;; SUBPROCESS START ;;;; |
169 | | - (define-values (egglog-process egglog-output egglog-in err) (create-new-egglog-subprocess)) |
| 169 | + (define subproc (create-new-egglog-subprocess dump-file)) |
170 | 170 |
|
171 | 171 | (thread (lambda () |
172 | 172 | (with-handlers ([exn:fail? (lambda (_) (void))]) |
173 | | - (for ([line (in-lines err)]) |
| 173 | + (for ([line (in-lines (egglog-subprocess-error subproc))]) |
174 | 174 | (void))))) |
175 | 175 |
|
176 | 176 | ;; Send whatever we have so far to egglog |
177 | 177 | ;; Expected no output anyways as there is no extraction |
178 | | - (send-to-egglog (get-current-program curr-program) |
179 | | - egglog-process |
180 | | - egglog-output |
181 | | - egglog-in |
182 | | - err |
183 | | - dump-file) |
| 178 | + (send-to-egglog (get-current-program curr-program) subproc) |
184 | 179 |
|
185 | 180 | ;; 4. Running the schedule : having code inside to emulate egraph-run-rules |
186 | 181 |
|
|
189 | 184 |
|
190 | 185 | (for ([tag (in-list tag-schedule)]) |
191 | 186 | (match tag |
192 | | - ['lift |
193 | | - (send-to-egglog (list '(run-schedule (saturate lift))) |
194 | | - egglog-process |
195 | | - egglog-output |
196 | | - egglog-in |
197 | | - err |
198 | | - dump-file)] |
199 | | - |
200 | | - ['lower |
201 | | - (send-to-egglog (list '(run-schedule (saturate lower))) |
202 | | - egglog-process |
203 | | - egglog-output |
204 | | - egglog-in |
205 | | - err |
206 | | - dump-file)] |
207 | | - |
208 | | - ['unsound |
209 | | - (send-to-egglog (list '(run-schedule (saturate unsound))) |
210 | | - egglog-process |
211 | | - egglog-output |
212 | | - egglog-in |
213 | | - err |
214 | | - dump-file)] |
215 | | - |
216 | | - ['rewrite |
217 | | - ;; Run the rewrite ruleset interleaved with const-fold until the best iteration |
218 | | - (egglog-unsound-detected-subprocess tag |
219 | | - egglog-process |
220 | | - egglog-output |
221 | | - egglog-in |
222 | | - err |
223 | | - dump-file)])) |
| 187 | + ['lift (send-to-egglog (list '(run-schedule (saturate lift))) subproc)] |
| 188 | + |
| 189 | + ['lower (send-to-egglog (list '(run-schedule (saturate lower))) subproc)] |
| 190 | + |
| 191 | + ['unsound (send-to-egglog (list '(run-schedule (saturate unsound))) subproc)] |
| 192 | + |
| 193 | + ;; Run the rewrite ruleset interleaved with const-fold until the best iteration |
| 194 | + ['rewrite (egglog-unsound-detected-subprocess tag subproc)])) |
224 | 195 |
|
225 | 196 | ;; 5. Extraction -> should just need constructor names from egglog-add-exprs |
226 | 197 | (define extract-commands |
|
234 | 205 |
|
235 | 206 | ;; Extract its returned value |
236 | 207 | (define stdout-content |
237 | | - (send-to-egglog extract-commands |
238 | | - egglog-process |
239 | | - egglog-output |
240 | | - egglog-in |
241 | | - err |
242 | | - dump-file |
243 | | - #:num-extracts (length extract-commands))) |
| 208 | + (send-to-egglog extract-commands subproc #:num-extracts (length extract-commands))) |
244 | 209 |
|
245 | 210 | ;; (Listof (Listof exprs)) |
246 | 211 | (define herbie-exprss |
|
255 | 220 | #:key batchref-idx))) |
256 | 221 |
|
257 | 222 | ;; Close everything subprocess related |
258 | | - (close-output-port egglog-in) |
259 | | - (close-input-port egglog-output) |
260 | | - (close-input-port err) |
261 | | - (subprocess-wait egglog-process) |
262 | | - (unless (eq? (subprocess-status egglog-process) 'done) |
263 | | - (subprocess-kill egglog-process #f)) |
| 223 | + (egglog-subprocess-close subproc) |
264 | 224 |
|
265 | 225 | ;; (Listof (Listof batchref)) |
266 | 226 | result) |
|
792 | 752 |
|
793 | 753 | (values (reverse all-bindings) curr-bindings)) |
794 | 754 |
|
795 | | -(define (egglog-unsound-detected-subprocess tag egglog-process egglog-output egglog-in err dump-file) |
| 755 | +(define (egglog-unsound-detected-subprocess tag subproc) |
796 | 756 |
|
797 | 757 | (define node-limit (*node-limit*)) |
798 | 758 | (define iter-limit (*default-egglog-iter-limit*)) |
|
833 | 793 |
|
834 | 794 | ;; Get egglog output |
835 | 795 | (define-values (math-unsound? math-node-limit? math-total-nodes) |
836 | | - (get-egglog-output math-schedule |
837 | | - egglog-process |
838 | | - egglog-output |
839 | | - egglog-in |
840 | | - err |
841 | | - node-limit |
842 | | - dump-file)) |
| 796 | + (get-egglog-output math-schedule subproc node-limit)) |
843 | 797 |
|
844 | 798 | (cond |
845 | 799 | ;; There are two condiitons where we exit unsoundness dteection WITHOUT running (pop) |
|
866 | 820 | ;; e-graph while extracting. For now, popping provides a smaller e-graph and gives |
867 | 821 | ;; performance comparable to Egg-Herbie, thought it doesn't affect correctness too much |
868 | 822 | [math-node-limit? |
869 | | - (send-to-egglog (list '(pop)) egglog-process egglog-output egglog-in err dump-file) |
| 823 | + (send-to-egglog (list '(pop)) subproc) |
870 | 824 | (values (sub1 curr-iter) #t)] |
871 | 825 |
|
872 | 826 | ;; If Unsoundness detected or node-limit reached, then return the |
873 | 827 | ;; optimal iter limit (one less than current) and run (pop) |
874 | 828 | [math-unsound? |
875 | 829 | ;; Pop once at the end since the egraph isn't valid |
876 | | - (send-to-egglog (list '(pop)) egglog-process egglog-output egglog-in err dump-file) |
| 830 | + (send-to-egglog (list '(pop)) subproc) |
877 | 831 |
|
878 | 832 | ;; Return one less than current iteration and indicate that we need to run again because pop |
879 | 833 | (values (sub1 curr-iter) #t)] |
|
892 | 846 | '(extract (bad-merge?)))) |
893 | 847 |
|
894 | 848 | (define-values (const-unsound? const-node-limit? const-total-nodes) |
895 | | - (get-egglog-output const-schedule |
896 | | - egglog-process |
897 | | - egglog-output |
898 | | - egglog-in |
899 | | - err |
900 | | - node-limit |
901 | | - dump-file)) |
| 849 | + (get-egglog-output const-schedule subproc node-limit)) |
902 | 850 |
|
903 | 851 | (cond |
904 | 852 | ;; TODO: See the TODO from above |
905 | 853 | [(equal? const-total-nodes prev-number-nodes) (values curr-iter #f)] |
906 | 854 | [const-node-limit? |
907 | | - (send-to-egglog (list '(pop)) egglog-process egglog-output egglog-in err dump-file) |
| 855 | + (send-to-egglog (list '(pop)) subproc) |
908 | 856 | (values (sub1 curr-iter) #t)] |
909 | 857 |
|
910 | 858 | [const-unsound? |
911 | | - (send-to-egglog (list '(pop)) egglog-process egglog-output egglog-in err dump-file) |
| 859 | + (send-to-egglog (list '(pop)) subproc) |
912 | 860 | (values (sub1 curr-iter) #t)] |
913 | 861 |
|
914 | 862 | [else |
|
917 | 865 |
|
918 | 866 | (loop (add1 curr-iter))])])]))) |
919 | 867 |
|
920 | | -(define (get-egglog-output curr-schedule |
921 | | - egglog-process |
922 | | - egglog-output |
923 | | - egglog-in |
924 | | - err |
925 | | - node-limit |
926 | | - dump-file) |
927 | | - (define-values (node-values unsound?) |
928 | | - (send-to-egglog-unsound-detection curr-schedule |
929 | | - egglog-process |
930 | | - egglog-output |
931 | | - egglog-in |
932 | | - err |
933 | | - dump-file)) |
| 868 | +(define (get-egglog-output curr-schedule subproc node-limit) |
| 869 | + (define-values (node-values unsound?) (send-to-egglog-unsound-detection curr-schedule subproc)) |
934 | 870 |
|
935 | 871 | ; (when unsound? |
936 | 872 | ; (printf "ALERT : UNSOUNDNESS DETECTED when...\n")) |
|
0 commit comments