From e737b513b5e0542b70d9838b9f660e545adeaa31 Mon Sep 17 00:00:00 2001 From: Sandeep Dasgupta Date: Thu, 7 Jun 2018 13:05:30 -0500 Subject: [PATCH] https://github.com/sdasgup3/binary-decompilation/issues/77: wip --- x86-semantics/scripts/run.pl | 72 +++++++++++++++++++-- x86-semantics/semantics/x86-configuration.k | 8 ++- x86-semantics/semantics/x86-env-init.k | 22 +++++++ x86-semantics/semantics/x86-semantics.k | 4 +- 4 files changed, 96 insertions(+), 10 deletions(-) diff --git a/x86-semantics/scripts/run.pl b/x86-semantics/scripts/run.pl index 6272a9f59..a38177a31 100755 --- 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,15 +67,73 @@ 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( @@ -81,8 +141,10 @@ sub createEnv { 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 index 4ca397d5f..b271c8d7d 100644 --- 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 configuration //initEnvironment(ListItem("a.out") ListItem("HelloWorld!") .List) ~> $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)) + */ /*@ diff --git a/x86-semantics/semantics/x86-env-init.k b/x86-semantics/semantics/x86-env-init.k index 059603f36..3adf25c3a 100644 --- 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 + initRegisters(.RegValPairList) => . + ... + rule + initRegisters(regvalpair(R:String, V:MInt ) Rest:RegValPairList) => + initRegisters(Rest) + ... + ... .Map => R |-> V ... + + + /*@ 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 index ab08bb066..980ecfa80 100644 --- 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