| 1 | #!/usr/bin/perl
|
|---|
| 2 | use Math::Round;
|
|---|
| 3 |
|
|---|
| 4 | $output_file = $ARGV[0];
|
|---|
| 5 |
|
|---|
| 6 | open(OUTPUT, "<", $output_file) || die "Could not open $output_file";
|
|---|
| 7 |
|
|---|
| 8 | while ($line=<OUTPUT>) {
|
|---|
| 9 | my($name,$tag,$message,$result);
|
|---|
| 10 |
|
|---|
| 11 | chomp($line);
|
|---|
| 12 | next unless ($line =~/^Check data race for/);
|
|---|
| 13 | ($name) = ($line =~/^Check data race for (.*)$/);
|
|---|
| 14 | $tag = -1;
|
|---|
| 15 | if ($name =~ /yes.c$/) {
|
|---|
| 16 | $tag = 1; # 1 for data race
|
|---|
| 17 | } elsif ($name =~ /-no.c$/) {
|
|---|
| 18 | $tag = 0; # 0 for free of data race
|
|---|
| 19 | }
|
|---|
| 20 | ## checking if printed lines are expected:
|
|---|
| 21 | $line=<OUTPUT>;
|
|---|
| 22 | chomp($line);
|
|---|
| 23 | ($line =~ /^civl verify/) || die "Unexpected line after reading the name of the benchmark.";
|
|---|
| 24 | $line=<OUTPUT>;
|
|---|
| 25 | chomp($line);
|
|---|
| 26 | ($line =~ /^CIVL v1.8\+ of/) || die "Unexpected line after echoing the command";
|
|---|
| 27 | $line=<OUTPUT>;
|
|---|
| 28 | chomp($line);
|
|---|
| 29 | if (($line =~ /^Error:/) || ($line =~ /^Exception in thread/)) {
|
|---|
| 30 | $result = "E";
|
|---|
| 31 | } elsif ($line =~ /^Possible data race under/) {
|
|---|
| 32 | ## static analyzer caught error
|
|---|
| 33 | if ($tag == 1) {
|
|---|
| 34 | $result = "P"
|
|---|
| 35 | } elsif ($tag == 0) {
|
|---|
| 36 | $result = "N";
|
|---|
| 37 | } else {
|
|---|
| 38 | die "Invalid tag though static analyzer catch error for $name at $line";
|
|---|
| 39 | }
|
|---|
| 40 | } else {
|
|---|
| 41 | ## look for civl results:
|
|---|
| 42 | while ($line=<OUTPUT>) {
|
|---|
| 43 | if ($line =~ /^CIVL execution violation/) {
|
|---|
| 44 | $message = $line,"\n",<OUTPUT>;
|
|---|
| 45 | }
|
|---|
| 46 | next unless ($line =~ /^=== Result ===/);
|
|---|
| 47 | $line=<OUTPUT>;
|
|---|
| 48 | if ($line =~ /^The standard properties hold for all executions.$/) {
|
|---|
| 49 | $result = $tag == 0 ? "P (CIVL)" : "N";
|
|---|
| 50 | } else {
|
|---|
| 51 | $result = $tag == 1 ? "P (CIVL)" : "N";
|
|---|
| 52 | ($line =~ /^The program MAY NOT be correct./) || die "Irregular CIVL output for false benchmarks: $line";
|
|---|
| 53 | }
|
|---|
| 54 | last;
|
|---|
| 55 | }
|
|---|
| 56 | }
|
|---|
| 57 |
|
|---|
| 58 | die "no name" unless defined($name);
|
|---|
| 59 | die "no tag" unless defined($tag);
|
|---|
| 60 | die "no result" unless defined($result);
|
|---|
| 61 |
|
|---|
| 62 | # for debugging:
|
|---|
| 63 |
|
|---|
| 64 | # print "name = $name\n";
|
|---|
| 65 | # print "cite = $cite\n";
|
|---|
| 66 | # print "type = $type\n";
|
|---|
| 67 | # print "scale = $scale\n";
|
|---|
| 68 | # print "loc = $loc\n";
|
|---|
| 69 | # print "prove = $prove\n";
|
|---|
| 70 | # print "mem = $mem\n";
|
|---|
| 71 | # print "time = $time\n";
|
|---|
| 72 | # print "states = $states\n"
|
|---|
| 73 | # print "transitions = $steps\n";
|
|---|
| 74 | # print "result = $result\n";
|
|---|
| 75 | # print "\n";
|
|---|
| 76 |
|
|---|
| 77 | printf("%-40s %s\n", $name, $result);
|
|---|
| 78 | if ($tag == 1 && $result == "P (CIVL)") {
|
|---|
| 79 | print $message, "\n";
|
|---|
| 80 | }
|
|---|
| 81 | }
|
|---|