#77: wip

sdasgup3 · Jun 7, 2018 · e737b51 · e737b51
1 parent 24de5ce
commit e737b51
Show file tree

Hide file tree

Showing 4 changed files with 96 additions and 10 deletions.
diff --git a/x86-semantics/scripts/run.pl b/x86-semantics/scripts/run.pl
@@ -21,6 +21,7 @@
 my $compare    = "";
 my $output     = "";
 my $linker     = "";
+my $testinput  = "";
 my @args       = ();
 my $kstateskip = 0;
 my $kdefn =
@@ -39,6 +40,7 @@
     "compare"      => \$compare,
     "clean"        => \$clean,
     "outdir:s"     => \$outdir,
+    "testinput:s"  => \$testinput,
     "kstateskip:s" => \$kstateskip,
     "linker:s"     => \$linker,
 ) or die("Error in command line arguments\n");
@@ -65,24 +67,84 @@ sub createEnv {
     return $cargs;
 }
 
+sub createRegArgs {
+
+    my $retVal =
+"'-cREGV= regvalpair(\"RIP\", mi(64, 0)) regvalpair(\"RAX\",  mi(64, 0)) regvalpair(\"RBX\"    , mi(64, 0)) regvalpair(\"RCX\"    , mi(64, 0)) regvalpair(\"RDX\"    , mi(64, 0)) regvalpair(\"RSI\"    , mi(64, 0)) regvalpair(\"RDI\"    , mi(64, 0)) regvalpair(\"RSP\"    , mi(64, 0)) regvalpair(\"RBP\"    , mi(64, 0)) regvalpair(\"R8\"     , mi(64, 0)) regvalpair(\"R9\"     , mi(64, 0)) regvalpair(\"R10\"    , mi(64, 0)) regvalpair(\"R11\"    , mi(64, 0)) regvalpair(\"R12\"    , mi(64, 0)) regvalpair(\"R13\"    , mi(64, 0)) regvalpair(\"R14\"    , mi(64, 0)) regvalpair(\"R15\"    , mi(64, 0)) regvalpair(\"CF\"     , mi(1, 0)) regvalpair(\"PF\" , mi(1, 0)) regvalpair(\"AF\"     , mi(1, 0)) regvalpair(\"ZF\"     , mi(1, 0)) regvalpair(\"SF\"     , mi(1, 0)) regvalpair(\"OF\"     , mi(1, 0)) regvalpair(\"YMM0\"   ,  mi(256, 0)) regvalpair(\"YMM1\"   ,  mi(256, 0)) regvalpair(\"YMM2\"   ,  mi(256, 0)) regvalpair(\"YMM3\"   ,  mi(256, 0)) regvalpair(\"YMM4\"   ,  mi(256, 0)) regvalpair(\"YMM5\"   ,  mi(256, 0)) regvalpair(\"YMM6\"   ,  mi(256, 0)) regvalpair(\"YMM7\"   ,  mi(256, 0)) regvalpair(\"YMM8\"   ,  mi(256, 0)) regvalpair(\"YMM9\"   ,  mi(256, 0)) regvalpair(\"YMM10\"  ,  mi(256, 0)) regvalpair(\"YMM11\"  ,  mi(256, 0)) regvalpair(\"YMM12\"  ,  mi(256, 0)) regvalpair(\"YMM13\"  ,  mi(256, 0)) regvalpair(\"YMM14\"  ,  mi(256, 0)) regvalpair(\"YMM15\"  ,  mi(256, 0))'";
+    if ( "" eq $testinput ) {
+        return $retVal;
+    }
+
+    open( my $fp, "<", $testinput ) or die "cannot open: $!";
+    my @lines = <$fp>;
+    close $fp;
+    $retVal = "'-cREGV= regvalpair(\"RIP\", mi(64, 0))";
+
+    for my $line (@lines) {
+        if ( $line =~ m/^%(\w+)\s+([\dabcdef].*)/ ) {
+            my $reg    = $1;
+            my $val    = utils::trim( $2, " " );
+            my $intval = 0;
+            my $size   = 0;
+
+            if ( $reg =~ m/rf/ ) {
+                next;
+            }
+            if ( $reg =~ m/^ymm/ ) {
+                $size = 256;
+            }
+            elsif ( $reg =~ m/^r/ ) {
+                $size = 64;
+            }
+            elsif ( $reg =~ m/af|cf|of|zf|sf|pf/ ) {
+                $size = 1;
+            }
+            else {
+                next;
+            }
+
+            $intval = utils::toDec( $val, $size );
+            my $reg_uc = uc($reg);
+
+            #print $reg_uc. " "
+            #  . $size
+            #  . "\n\t\t"
+            #  . $val
+            #  . "\n\t\t$intval" . "\n";
+            $retVal = $retVal . " regvalpair(\"$reg_uc\", mi($size, $intval))";
+        }
+    }
+    $retVal = $retVal . "'";
+    return $retVal;
+}
+
+#sub generateOutTC {
+#  my $outFile = shift @_;
+#
+#}
+
 if ( "" ne $krun ) {
     my ( $dir, $basename, $ext ) = utils::split_filename($file);
 
-    $output = "$outdir/$basename.kstate";
+    #$output = "$outdir/$basename.kstate";
 
     my $envArgs = createEnv( \@args );
+    my $regArgs = createRegArgs();
     execute(
-        "time krun -d $kdefn $basename.$ext $envArgs --output-file $output",
-        1 );
+"time krun -d $kdefn $basename.$ext $envArgs $regArgs --output-file $output",
+        1
+    );
 
     my ( $fh_unused, $tmpfile ) = tempfile( "tmpfileXXXXX", DIR => "/tmp/" );
     execute(
 "cat $output | sed  '/^\\s*\$/d' | sed 's/(\\s*\"/(\\n\"/g'  1> $tmpfile  2>&1 &&  mv $tmpfile $output",
         1
     );
 
-    #execute( "", 1 );
-    checkKRunStatus("$outdir/$basename.kstate");
+    #checkKRunStatus("$outdir/$basename.kstate");
+    checkKRunStatus("$output");
+
+    #generateOutTC($output);
 }
 
 if ( "" ne $xrun ) {

diff --git a/x86-semantics/semantics/x86-configuration.k b/x86-semantics/semantics/x86-configuration.k
@@ -15,11 +15,13 @@ module X86-CONFIGURATION
   imports X86-LOADER-SYNTAX
   //imports COMMON-C-LIBRARY-CONFIGURATION
 
+
   // configuration <T>
   configuration
 //initEnvironment(ListItem("a.out") ListItem("HelloWorld!") .List) ~> 
     <k> 
 	$PGM:Instructions ~> 
+	initRegisters($REGV:RegValPairList) ~> 
 	initEnvironment($ARGV:List) ~> 
         loadEntryPoint ~>
 	inforegisters ~> 
@@ -47,7 +49,6 @@ module X86-CONFIGURATION
       .Map
       /*@
         General purpose registers.
-      */
       ("RIP" |-> mi(64, 0))
       ("RAX" |-> mi(64, 0))
       ("RBX" |-> mi(64, 0))
@@ -65,20 +66,20 @@ module X86-CONFIGURATION
       ("R13" |-> mi(64, 0))
       ("R14" |-> mi(64, 0))
       ("R15" |-> mi(64, 0))
+      */
 
       /*@
         General purpose registers.
-      */
       ("CF" |-> mi(1, 0))
       ("PF" |-> mi(1, 0))
       ("AF" |-> mi(1, 0))
       ("ZF" |-> mi(1, 0))
       ("SF" |-> mi(1, 0))
       ("OF" |-> mi(1, 0))
+      */
 
       /*@
         256 bit ymm registers
-      */
       ("YMM0"  |->  mi(256, 0))
       ("YMM1"  |->  mi(256, 0))
       ("YMM2"  |->  mi(256, 0))
@@ -95,6 +96,7 @@ module X86-CONFIGURATION
       ("YMM13" |->  mi(256, 0))
       ("YMM14" |->  mi(256, 0))
       ("YMM15" |->  mi(256, 0))
+      */
     </regstate>
 
     /*@

diff --git a/x86-semantics/semantics/x86-env-init.k b/x86-semantics/semantics/x86-env-init.k
@@ -2,13 +2,34 @@ require "x86-configuration.k"
 
 module X86-INIT-SYNTAX
   imports LIST
+  imports STRING
+  imports MINT
+
+  syntax RegValPair ::= "regvalpair" "(" String "," MInt ")"
+  syntax RegValPairList ::= List{RegValPair, ""} [klabel(regvalpairlist)]
+
 
   syntax KItem ::= initEnvironment(List)
+  syntax KItem ::= initRegisters(RegValPairList)
 endmodule
 
 module X86-INIT
   imports X86-CONFIGURATION
 
+  /*@
+    Initialize register with user supplied values.
+  */
+  rule <k> 
+    initRegisters(.RegValPairList) => .  
+  ...</k>
+  rule <k>
+      initRegisters(regvalpair(R:String, V:MInt ) Rest:RegValPairList) => 
+        initRegisters(Rest)
+  ...</k>
+      <regstate>...  .Map => R |-> V    ...</regstate>
+
+
+
   /*@
     Initialization involves:
     1. Allocating stack and environment memory (16 bytes alligned)
@@ -17,6 +38,7 @@ module X86-INIT
   rule initEnvironment(L:List) =>
      allocateStackMemory(256, 16 *Int 8) ~> initReturnFromEntryFunction ~> initArgc(mySize(L)) ~> initArgv(L)
 
+
   /*@
     Store a fake return adress mi(64, -1) which signals program executaion halt. 
   */  

diff --git a/x86-semantics/semantics/x86-semantics.k b/x86-semantics/semantics/x86-semantics.k
@@ -3,7 +3,7 @@ require "x86-env-init.k"
 require "x86-fetch-execute.k"
 require "x86-abstract-semantics.k"
 require "x86-flag-checks.k"
-require "x86-verification-lemmas.k"
+//require "x86-verification-lemmas.k"
 require "x86-instructions-semantics.k"
 require "x86-memory.k"
 require "x86-mint-wrapper.k"
@@ -15,7 +15,7 @@ module X86-SEMANTICS
   imports X86-FETCH-EXECUTE
   imports X86-ABSTRACT-SEMANTICS
   imports X86-FLAG-CHECKS
-  imports X86-VERIFICATION-LEMMAS
+  //imports X86-VERIFICATION-LEMMAS
   imports X86-INSTRUCTIONS-SEMANTICS
   imports X86-MEMORY
   imports MINT-WRAPPER