|
1 # |
|
2 # Author: Jasmin Blanchette and Sascha Boehme |
|
3 # |
|
4 # Testing tool for automated proof tools. |
|
5 # |
|
6 |
|
7 use File::Basename; |
|
8 |
|
9 # environment |
|
10 |
|
11 my $isabelle_home = $ENV{'ISABELLE_HOME'}; |
|
12 my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; |
|
13 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; |
|
14 my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; |
|
15 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; |
|
16 my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; |
|
17 |
|
18 my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; |
|
19 |
|
20 |
|
21 # arguments |
|
22 |
|
23 my $actions = $ARGV[0]; |
|
24 |
|
25 my $thy_file = $ARGV[1]; |
|
26 my $start_line = "0"; |
|
27 my $end_line = "~1"; |
|
28 if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { |
|
29 $thy_file = $1; |
|
30 $start_line = $2; |
|
31 $end_line = $3; |
|
32 } |
|
33 my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); |
|
34 my $new_thy_name = $thy_name . "_Mirabelle"; |
|
35 my $new_thy_file = $output_path . "/" . $new_thy_name . $ext; |
|
36 |
|
37 |
|
38 # setup |
|
39 |
|
40 my $setup_thy_name = $thy_name . "_Setup"; |
|
41 my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; |
|
42 my $log_file = $output_path . "/" . $thy_name . ".log"; |
|
43 |
|
44 my @action_files; |
|
45 my @action_names; |
|
46 foreach (split(/:/, $actions)) { |
|
47 if (m/([^[]*)/) { |
|
48 push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; |
|
49 push @action_names, $1; |
|
50 } |
|
51 } |
|
52 my $tools = ""; |
|
53 if ($#action_files >= 0) { |
|
54 $tools = "uses " . join(" ", @action_files); |
|
55 } |
|
56 |
|
57 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'"; |
|
58 |
|
59 print SETUP_FILE <<END; |
|
60 theory "$setup_thy_name" |
|
61 imports "$mirabelle_thy" "$mirabelle_theory" |
|
62 $tools |
|
63 begin |
|
64 |
|
65 setup {* |
|
66 Config.put_thy Mirabelle.logfile "$log_file" #> |
|
67 Config.put_thy Mirabelle.timeout $timeout #> |
|
68 Config.put_thy Mirabelle.start_line $start_line #> |
|
69 Config.put_thy Mirabelle.end_line $end_line |
|
70 *} |
|
71 |
|
72 END |
|
73 |
|
74 foreach (split(/:/, $actions)) { |
|
75 if (m/([^[]*)(?:\[(.*)\])?/) { |
|
76 my ($name, $settings_str) = ($1, $2 || ""); |
|
77 $name =~ s/^([a-z])/\U$1/; |
|
78 print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; |
|
79 my $sep = ""; |
|
80 foreach (split(/,/, $settings_str)) { |
|
81 if (m/\s*(.*)\s*=\s*(.*)\s*/) { |
|
82 print SETUP_FILE "$sep(\"$1\", \"$2\")"; |
|
83 $sep = ", "; |
|
84 } |
|
85 } |
|
86 print SETUP_FILE "] *}\n"; |
|
87 } |
|
88 } |
|
89 |
|
90 print SETUP_FILE "\nend"; |
|
91 close SETUP_FILE; |
|
92 |
|
93 |
|
94 # modify target theory file |
|
95 |
|
96 open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'"; |
|
97 my @lines = <OLD_FILE>; |
|
98 close(OLD_FILE); |
|
99 |
|
100 my $thy_text = join("", @lines); |
|
101 my $old_len = length($thy_text); |
|
102 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g; |
|
103 $thy_text =~ s/(imports)(\s+)/$1 "$setup_thy_name"$2/g; |
|
104 die "No 'imports' found" if length($thy_text) == $old_len; |
|
105 |
|
106 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'"; |
|
107 print NEW_FILE $thy_text; |
|
108 close(NEW_FILE); |
|
109 |
|
110 my $root_file = "$output_path/ROOT_$thy_name.ML"; |
|
111 open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'"; |
|
112 print ROOT_FILE "use_thy \"$output_path/$new_thy_name\";\n"; |
|
113 close(ROOT_FILE); |
|
114 |
|
115 |
|
116 # run isabelle |
|
117 |
|
118 open(LOG_FILE, ">$log_file"); |
|
119 print LOG_FILE "Run of $new_thy_file with:\n"; |
|
120 foreach $name (@action_names) { |
|
121 print LOG_FILE " $name\n"; |
|
122 } |
|
123 close(LOG_FILE); |
|
124 |
|
125 my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " . |
|
126 "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n"; |
|
127 |
|
128 |
|
129 # cleanup |
|
130 |
|
131 unlink $root_file; |
|
132 unlink $setup_file; |
|
133 |
|
134 exit $r; |
|
135 |