program-runner

#!/usr/bin/env perl
use strict;
use warnings;

use List::Util qw(reduce);
use File::Spec::Functions qw(catfile);
use File::Temp;
use File::Copy;
use MIME::Base64;
use String::Escape qw(quote backslash); 

setpgrp;

# We trap control-c (and others) so we can clean up when that happens.
$SIG{'ABRT'} = 'interruptHandler';
$SIG{'TERM'} = 'interruptHandler';
$SIG{'QUIT'} = 'interruptHandler';
$SIG{'SEGV'} = 'interruptHandler';
$SIG{'HUP' } = 'interruptHandler';
$SIG{'TRAP'} = 'interruptHandler';
$SIG{'STOP'} = 'interruptHandler';
$SIG{'INT'} = 'interruptHandler'; # handle control-c 

# Set heap and stack size of krun

my $HEAP_SIZE = '__EXTERN_HEAP_SIZE__';

$ENV{K_OPTS} = "-Xms64m -Xmx$HEAP_SIZE -Xss32m -XX:+TieredCompilation";

my $SCRIPTS_DIR = '__EXTERN_SCRIPTS_DIR__';

my $KRUN = '__EXTERN_KRUN__';

my $EXEC_DEF = catfile($SCRIPTS_DIR, "c-cpp-kompiled");
my $EXEC_ND_DEF = catfile($SCRIPTS_DIR, "c-nd-kompiled");
my $EXEC_ND_THREAD_DEF = catfile($SCRIPTS_DIR, "c-nd-thread-kompiled");

my @temporaryFiles = ();

exit main();

sub main {
      my $fileInput = File::Temp->new(
            TEMPLATE => 'tmp-kcc-in-XXXXXXXXXXX', 
            SUFFIX => '.bin', 
            UNLINK => 0);
      my $objInput = File::Temp->new(
            TEMPLATE => 'tmp-kcc-in-XXXXXXXXXXX',
            SUFFIX => '.o',
            UNLINK => 0);
      my $fileOutput = File::Temp->new(
            TEMPLATE => 'tmp-kcc-out-XXXXXXXXXXX', 
            SUFFIX => '.txt', 
            UNLINK => 0);

      push(@temporaryFiles, $fileInput);
      push(@temporaryFiles, $objInput);
      push(@temporaryFiles, $fileOutput);

      print $fileInput decode_base64(linkedProgram());
      if (defined nativeObjFile()) {
        print $objInput decode_base64(nativeObjFile());
      } else {
        $objInput = '';
      }

      my $argv = reduce { our ($a, $b); "`_List_`($a,$b)" } (map {qq|`ListItem`(#token($_, "String"))|} (map {quote(backslash(quote(backslash($_))))} ($0, @ARGV)));

      my @cmd = ('--output', 'kast', '--no-sort-collections', '--no-alpha-renaming', '-d', $EXEC_DEF, "-cARGV=$argv", '-pARGV=printf %s', '-w', 'none', '--parser',
                 'cat', $fileInput);
      my $options = getOptions();

      if (defined $ENV{HELP}) {
            print "Here are some configuration variables you can set to affect how this program is run:\n";
            print "DEBUG --- runs krun with the --debug flag.\n";
            print "TRACE --- runs krun with the --trace flag.\n";
            print "DUMPALL --- leaves all the intermediate files in the current directory.\n";
            print "LTLMC --- LTL model checking.\n";
            print "VERBOSE --- verbose output.\n";
            print "PROVE=<file> --- enable prover on specification file.\n";
            print "E.g., DEBUG=1 $0\n";
            print "\n";
            print "This message was displayed because the variable HELP was set.  Use HELP=1 $0 to turn off.\n";
            return 1;
      }

      if (defined $ENV{TRACE}) {
           push @cmd, '--trace';
      }

      if (defined $ENV{DEBUG}) {
           push @cmd, '--debug';
      }

      if (defined $ENV{VERBOSE}) {
           push @cmd, '--verbose';
      }

      push @cmd, '--native-libraries';
      my $libs = nativeLibraries();
      # kcc may have been run as k++ so this is necessary
      push @cmd, "-lstdc++ $libs $objInput";

      if (defined $ENV{DEPTH}) {
            push @cmd, '--depth';
            push @cmd, $ENV{DEPTH};
      }

      if (defined $ENV{PROVE}) {
            push @cmd, '--prove';
            push @cmd, $ENV{PROVE};
            push @cmd, '--smt_prelude';
            push @cmd, $ENV{SMT_PRELUDE};
      } else {
            push @cmd, '--smt';
            push @cmd, 'none';
            push @cmd, '--output-file';
            push @cmd, $fileOutput;
      }

      if (defined $ENV{SEARCH}) {
            push @cmd, '--search-final';
            $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)";
            push @cmd, '-d';
            push @cmd, $EXEC_ND_DEF;
            print 'Searching reachable states... ';
            print "(with non-deterministic expression sequencing)\n";
      }

      if (defined $ENV{THREADSEARCH}) {
            push @cmd, '--search-final';
            $options = "`_Set_`(`SetItem`(`NoIO`(.KList)), $options)";
            push @cmd, '-d';
            push @cmd, $EXEC_ND_THREAD_DEF;
            print 'Searching reachable states... ';
            print "(with non-deterministic thread interleaving)\n";
      }

      my $encodedJson = getJson();

      push @cmd, "-cOPTIONS=$options";
      push @cmd, '-pOPTIONS=printf %s';
      push @cmd, '-cJSON=#token(' . $encodedJson . ', "String")';
      push @cmd, '-pJSON=printf %s';

      # Execute krun with the arguments in @cmd
      print("'krun' '" . join("' '", @cmd) . "'\n") if defined $ENV{VERBOSE};
      my $ret = system($KRUN, @cmd) >> 8;

      if (defined $ENV{LTLMC} | defined $ENV{PROVE}) {
            return 0;
      }

      return processResult($fileOutput, $ret, defined $ENV{VERBOSE});
}

# TODO(chathhorn): We have two functions here because of the newlines -- the
# regexes below match against the whole file as opposed to a line at a time.
sub parseResult {
      my ($parsed) = (@_);

      /<k>(.*?)<\/k>/s && do {
            $parsed->{finalComp} = $1;
      };

      /<error-cell>\s*"(.*)"\s*<\/error-cell>/ && do {
            $parsed->{haveError} = 1;
            my $output = $1;
            $output =~ s/\%/\%\%/g;
            $output =~ s/`/\\`/g;
            $output =~ s/\\\\/\\\\\\\\/g;
            $parsed->{errorMsg} = substr(`printf "x$output"`, 1);
      };

      /<curr-function>\s*(Identifier \( "(.*?)" \)|(file-scope))\s*<\/curr-function>/ && do {
            $parsed->{errorFunc} = $2;
      };

      /<curr-program-loc>\s*CabsLoc\s*\(\s*"(.*)"\s*,\s*(\d+)\s*,\s*(\d+)\s*,\s*(\d+)\s*\)\s*<\/curr-program-loc>/ && do {
            $parsed->{errorFile} = $1;
            $parsed->{errorLine} = $2;
      };

      /<final-computation>(.*?)<\/final-computation>/s && do {
            $parsed->{finalComp} = $1;
      };

      /<computation>(.*?)<\/computation>/s && do {
            $parsed->{finalCompGoto} = $1;
      };

      /<type>(.*?)<\/type>/s && do {
            $parsed->{finalCompType} = $1;
      };

      /<output>\s*#buffer\s*\(\s*"(.*)"\s*\)\s*<\/output>/ && do {
            $parsed->{output} = $1;
      };

      /<result-value>\s*(-?\d+)\s*<\/result-value>/ && do {
            $parsed->{exitCode} = $1;
      };

      /<result-value>\s*NullPointer\s*<\/result-value>/ && do {
            $parsed->{exitCode} = 0;
      };
}

sub unindent {
      my ($str) = (@_);

      my @lines = split "\n", $str;

      for (@lines) {
            s/^\s+//;
      }

      return join "\n", @lines;
}

sub processResult {
      my ($fileOutput, $ret, $verbose) = (@_);
      my %parsed;

      open(OUT, "<$fileOutput");
      local $/;
      local $_ = <OUT>;
      print if $verbose;
      return $ret;
}

sub getAttribs {
      my ($nodeId, $errorStates, $goodFinal) = (@_);
      my $attribs = {};
      if (exists($errorStates->{$nodeId})) {
            $attribs->{"fillcolor"} = "red";
            $attribs->{"style"} = "filled";
      }
      if (exists($goodFinal->{$nodeId})) {
            $attribs->{"fillcolor"} = "green";
            $attribs->{"style"} = "filled";
      }
      return $attribs;
}

sub getString {
      my ($s) = (@_);

      return '' unless defined $s;

      $s =~ s/\%/\%\%/g;
      $s =~ s/\\\\/\\\\\\\\/g;
      return substr(`printf "x$s"`, 1);
}

sub interruptHandler {
      # Call single cleanup point.
      finalCleanup();
      kill 1, -$$;
      # Since we were interrupted, we should exit with a non-zero code.
      exit 1;
}

# This subroutine can be used as a way to ensure we clean up all resources
# whenever we exit. This is going to be mostly temp files. If the program
# terminates for almost any reason, this code will be executed.
sub finalCleanup {
      if (!defined $ENV{DUMPALL}) {
            for (@temporaryFiles) {
                  close $_;
                  unlink;
            }
      }
}

# This block gets run at the end of a normally terminating program, whether it
# simply exits, or dies. We use this to clean up.
END {
      # $? contains the value the program would normally have exited with.
      my $retval = $?;
      # Call single cleanup point.
      finalCleanup();
      exit $retval;
}

# The parsed file contents of the program to execute with krun gets appended.