source: CIVL/examples/omp/DataRaceBench/parse.pl@ e5cec5ae

1.23 2.0 main test-branch
Last change on this file since e5cec5ae was 143b174, checked in by Ziqing Luo <ziqing@…>, 9 years ago

add results parsing script and Makefile for data race benchmarks

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@4226 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100755
File size: 2.2 KB
RevLine 
[143b174]1#!/usr/bin/perl
2use Math::Round;
3
4$output_file = $ARGV[0];
5
6open(OUTPUT, "<", $output_file) || die "Could not open $output_file";
7
8while ($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}
Note: See TracBrowser for help on using the repository browser.