1 #!/usr/bin/env perl |
|
2 # |
|
3 # Author: Sascha Boehme, TU Muenchen |
|
4 # |
|
5 # Cache for prover results, based on discriminating problems using MD5. |
|
6 |
|
7 use strict; |
|
8 use warnings; |
|
9 use Digest::MD5; |
|
10 |
|
11 |
|
12 # arguments |
|
13 |
|
14 my $certs_file = shift @ARGV; |
|
15 my $location = shift @ARGV; |
|
16 my $result_file = pop @ARGV; |
|
17 my $problem_file = $ARGV[-1]; |
|
18 |
|
19 my $use_certs = not ($certs_file eq "-"); |
|
20 |
|
21 |
|
22 # create MD5 problem digest |
|
23 |
|
24 my $problem_digest = ""; |
|
25 if ($use_certs) { |
|
26 my $md5 = Digest::MD5->new; |
|
27 open FILE, "<$problem_file" or |
|
28 die "ERROR: Failed to open '$problem_file' ($!)"; |
|
29 $md5->addfile(*FILE); |
|
30 close FILE; |
|
31 $problem_digest = $md5->b64digest; |
|
32 } |
|
33 |
|
34 |
|
35 # lookup problem digest among existing certificates and |
|
36 # return a cached result (if there is a certificate for the problem) |
|
37 |
|
38 if ($use_certs and -e $certs_file) { |
|
39 my $cached = 0; |
|
40 open CERTS, "<$certs_file" or die "ERROR: Failed to open '$certs_file' ($!)"; |
|
41 while (<CERTS>) { |
|
42 if (m/(\S+) (\d+)/) { |
|
43 if ($1 eq $problem_digest) { |
|
44 my $start = tell CERTS; |
|
45 open FILE, ">$result_file" or |
|
46 die "ERROR: Failed to open '$result_file ($!)"; |
|
47 while ((tell CERTS) - $start < $2) { |
|
48 my $line = <CERTS>; |
|
49 print FILE $line; |
|
50 } |
|
51 close FILE; |
|
52 $cached = 1; |
|
53 last; |
|
54 } |
|
55 else { seek CERTS, $2, 1; } |
|
56 } |
|
57 else { die "ERROR: Invalid file format in '$certs_file'"; } |
|
58 } |
|
59 close CERTS; |
|
60 if ($cached) { exit 0; } |
|
61 } |
|
62 |
|
63 |
|
64 # invoke (remote or local) prover |
|
65 |
|
66 my $result; |
|
67 |
|
68 if ($location eq "remote") { |
|
69 $result = system "$ENV{'REMOTE_SMT'} @ARGV >$result_file 2>&1"; |
|
70 } |
|
71 elsif ($location eq "local") { |
|
72 $result = system "@ARGV >$result_file 2>&1"; |
|
73 } |
|
74 else { die "ERROR: No SMT solver invoked"; } |
|
75 |
|
76 |
|
77 # cache result |
|
78 |
|
79 if ($use_certs) { |
|
80 open CERTS, ">>$certs_file" or |
|
81 die "ERROR: Failed to open '$certs_file' ($!)"; |
|
82 print CERTS |
|
83 ("$problem_digest " . ((-s $result_file) + (length "\n")) . "\n"); |
|
84 |
|
85 open FILE, "<$result_file" or |
|
86 die "ERROR: Failed to open '$result_file' ($!)"; |
|
87 foreach (<FILE>) { print CERTS $_; } |
|
88 close FILE; |
|
89 |
|
90 print CERTS "\n"; |
|
91 close CERTS; |
|
92 } |
|
93 |
|