1#
2# Author: Jasmin Blanchette and Sascha Boehme
3#
4# Testing tool for automated proof tools.
5#
6
7use File::Basename;
8
9# environment
10
11my $isabelle_home = $ENV{'ISABELLE_HOME'};
12my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
13my $mirabelle_dir = $ENV{'MIRABELLE_DIR'};
14my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
15my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
16my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
17my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
18my $be_quiet = $ENV{'MIRABELLE_QUIET'};
19my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'};
20my $actions = $ENV{'MIRABELLE_ACTIONS'};
21
22my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
23
24
25# argument
26
27my $thy_file = $ARGV[0];
28
29my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
30my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
31my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
32my $new_thy_file = $path . "/" . $new_thy_name . $ext;
33
34
35# setup
36
37my $setup_file;
38my $setup_full_name;
39
40if (-e $user_setup_file) {
41  $setup_file = undef;
42  my ($name, $path, $ext) = fileparse($user_setup_file, ".thy");
43  $setup_full_name = $path . "/" . $name;
44}
45else {
46
47my $start_line = "0";
48my $end_line = "~1";
49if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
50  $thy_file = $1;
51  $start_line = $2;
52  $end_line = $3;
53}
54
55my $setup_thy_name = $thy_name . "_Setup";
56my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
57my $log_file = $output_path . "/" . $thy_name . ".log";
58
59my @action_files;
60my @action_names;
61foreach (split(/:/, $actions)) {
62  if (m/([^[]*)/) {
63    push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
64    push @action_names, $1;
65  }
66}
67my $tools = "";
68if ($#action_files >= 0) {
69  # uniquify
70  my $s = join ("\n", @action_files);
71  my @action_files = split(/\n/, $s . "\n" . $s);
72  %action_files = sort(@action_files);
73  $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files))));
74}
75
76open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
77
78print SETUP_FILE <<END;
79theory "$setup_thy_name"
80imports "$mirabelle_thy" "$mirabelle_theory"
81begin
82
83$tools
84
85setup {*
86  Config.put_global Mirabelle.logfile "$log_file" #>
87  Config.put_global Mirabelle.timeout $timeout #>
88  Config.put_global Mirabelle.start_line $start_line #>
89  Config.put_global Mirabelle.end_line $end_line
90*}
91
92END
93
94@action_list = split(/:/, $actions);
95
96foreach (reverse(@action_list)) {
97  if (m/([^[]*)(?:\[(.*)\])?/) {
98    my ($name, $settings_str) = ($1, $2 || "");
99    $name =~ s/^([a-z])/\U$1/;
100    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
101    my $sep = "";
102    foreach (split(/,/, $settings_str)) {
103      if (m/\s*([^=]*)\s*=\s*(.*)\s*/) {
104        print SETUP_FILE "$sep(\"$1\", \"$2\")";
105        $sep = ", ";
106      }
107      elsif (m/\s*(.*)\s*/) {
108        print SETUP_FILE "$sep(\"$1\", \"\")";
109        $sep = ", ";
110      }
111    }
112    print SETUP_FILE "] *}\n";
113  }
114}
115
116print SETUP_FILE "\nend";
117close SETUP_FILE;
118
119$setup_full_name = $output_path . "/" . $setup_thy_name;
120
121open(LOG_FILE, ">$log_file");
122print LOG_FILE "Run of $new_thy_file with:\n";
123foreach $action  (@action_list) {
124  print LOG_FILE "  $action\n";
125}
126close(LOG_FILE);
127
128}
129
130
131# modify target theory file
132
133open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
134my @lines = <OLD_FILE>;
135close(OLD_FILE);
136
137my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000);
138
139my $thy_text = join("", @lines);
140my $old_len = length($thy_text);
141$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
142$thy_text =~ s/\b$thy_name\./$new_thy_name./g;
143$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
144die "No 'imports' found" if length($thy_text) == $old_len;
145
146open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
147print NEW_FILE $thy_text;
148close(NEW_FILE);
149
150
151# run isabelle
152
153my $quiet = "";
154my $output_log = 1;
155if (defined $be_quiet and $be_quiet ne "") {
156  $quiet = " > /dev/null 2>&1";
157  $output_log = 0;
158}
159
160if ($output_log) { print "Mirabelle: $thy_file\n"; }
161
162my $cmd =
163  "isabelle process -o quick_and_dirty -o threads=1" .
164  " -T \"$path/$new_thy_name\" " .
165  ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") .
166  "-l $mirabelle_logic" . $quiet;
167my $result = system "bash", "-c", $cmd;
168
169if ($output_log) {
170  my $outcome = ($result ? "failure" : "success");
171  print "\nFinished:  $thy_file  [$outcome]\n";
172}
173
174
175# cleanup
176
177if (defined $setup_file) {
178  unlink $setup_file;
179}
180unlink $new_thy_file;
181
182exit ($result ? 1 : 0);
183