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