Script to remove legacy asserts

May 25, 2010 at 3:37 PM

Dear all,

in case this is useful attached is a brute force script to remove useless asserts by disabling them one-by-one (run overnight) ...

#!/usr/bin/perl

# Remove one-line asserts/requires when they are not needed.
# Might be helpful for reading legacy code (e.g. by a fellow
# verification engineer), but more proof-of-concept.
# Used with VCC (vcc.codeplex.com) in a Cygwin environment. 
# Reads in file, returns code with asserts commented out to stdout.
# Quick hack, no quality control, no ownership claimed, e.g. feel free to 
# alter. 
# (E.g. the voluntary restriction to one-line asserts to avoid false postives.)
# (Of course the right way to do this is would be to operate on the 
# abstract syntax tree.)
# Shotgun approach: disable asserts one by one, see if we still run.
# Warning: creates (without checking for overwrite) files called
# "*TMPFILE*" in directory with the code.
# The line "system" contains the actuall call to VCC (adapt to your needs).
# Arguments:
# (1) file to operate on; if given (2) function to operate on, (3) first line of function, (4) last line of function

if ($#ARGV == -1) {
    print "Usage: file [optionally: function begin end]\n";
}

# File to operate on.
my $file = $ARGV[0];

# The rest is optional.
my $function = $ARGV[1];
my $begin = $ARGV[2];
my $end = $ARGV[3];

use strict;

my $jitter = 1.0; # maximal allowed time use increase in seconds on assert removal
my $timeout = 500; # timeout in seconds

# create file, run vcc on it

sub do_file {

	my ($file_name, $file_lines, $function) = @_;
	open TMPFILE, ">$file_name";
	print TMPFILE join("", @$file_lines); 
	close TMPFILE;	    
    my $function_string = "";
    if (defined($function)) {
        $function_string = "/functions:$function";
    }
    return system("vcc /st /z3:/T:$timeout /a /b:/errorLimit:1 /ps:32 /b:/smoke $file_name $function_string > $file_name.result");

}

# get time used from output

sub get_time {

	my ($file_name) = @_;
	my $time;
	open TMPFILE, "$file_name";
	while (my $line = <TMPFILE>) {
		if ($line =~ /^Time: (\d+),(\d+)s total/) {
			$time = "$1.$2";
		}	
	}
	close TMPFILE;		
	return $time;
}

sub assert {

	my ($lines, $function, $begin, $end) = @_;
	
	my @tmplines = @$lines;
	# test that file is ok (otherwise no point in testing asserts)
	if (do_file("$file.TMPFILE", \@tmplines, $function) != 0) {
		# error
		return 0;
	};

	my $duration = get_time("$file.TMPFILE.result");

    if (!defined($begin)) {
        $begin = 0;
        $end = $#$lines;
    } else {
        $begin = int($begin);
        $end = int($end);
    }
	for (my $i = $begin; $i <= $end; $i++) {
    
		if ($$lines[$i] !~ /^\s*assert\(/ && $$lines[$i] !~ /^\s*requires\(/) {
			# (probably) not an assert and not a requires
			next;
		}

		# multiline assert treatment (recognition depending on your 
		# coding conventions) might go in here

		# ok, we've (probably) got an assert line which we want to 
		# check whether we can disable it
		my @tmplines = @$lines;
		$tmplines[$i] = "//" . $tmplines[$i] . "//VCC not needed"; 
		if (do_file("$file.TMPFILE.$i", \@tmplines, $function) == 0) {
			# still verifies with assert commented out, thus assert not needed
			# check timing
			my $new_duration = get_time("$file.TMPFILE.$i.result");
			my $return;
			chomp $$lines[$i];
			if ($$lines[$i] =~ /\r$/) {
				$return = chop $$lines[$i];
			}
			if ($new_duration < $duration + $jitter) {
				$$lines[$i] = "//$$lines[$i] //VCC assert not needed ($duration) ($new_duration)$return\n";
				$duration = $new_duration;
			} else {
				chomp $$lines[$i];
				$$lines[$i] = "$$lines[$i] //VCC assert needed for timing ($duration) ($new_duration)$return\n";
			}
		};
	}
	
} 

open FILE, $file || die "can't open $file";
my @lines = <FILE>;
assert(\@lines, $function, $begin, $end);
close FILE;

print @lines;

Coordinator
May 25, 2010 at 9:03 PM

Just a quick note:

if ($line =~ /^Time: (\d+),(\d+)s total/) {

should match for [,.] to allow for English locale as well (where VCC would output, e.g., 10.28s).

Best, Mark