Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 213 insertions, 0 deletions

diff --git a/test/lib/llvm.exp b/test/lib/llvm.exp
new file mode 100644
index 00000000..2857dd82
--- /dev/null
+++ b/test/lib/llvm.exp
@@ -0,0 +1,213 @@
+# This procedure executes one line of a test case's execution script.
+proc execOneLine { test PRS outcome lineno line } {
+  set status 0
+  set resultmsg ""
+  set retval [ catch { eval exec -keepnewline -- $line } errmsg ]
+  if { $retval != 0 } {
+    set code [lindex $::errorCode 0]
+    set lineno [expr $lineno + 1]
+    if { $PRS != ""} {
+      set PRS " for $PRS" 
+    }
+    set errmsg " at line $lineno\nwhile running: $line\n$errmsg"
+    switch "$code" {
+      CHILDSTATUS {
+        set status [lindex $::errorCode 2]
+        if { $status != 0 } {
+          set resultmsg "$test$PRS\nFailed with exit($status)$errmsg"
+        }
+      }
+      CHILDKILLED {
+        set signal [lindex $::errorCode 2]
+        set resultmsg "$test$PRS\nFailed with signal($signal)$errmsg"
+      }
+      CHILDSUSP {
+        set signal [lindex $::errorCode 2]
+        set resultmsg "$test$PRS\nFailed with suspend($signal)$errmsg"
+      }
+      POSIX {
+        set posixNum [lindex $::errorCode 1]
+        set posixMsg [lindex $::errorCode 2]
+        set resultmsg "$test$PRS\nFailed with posix($posixNum,$posixMsg)$errmsg"
+      }
+      NONE {
+      }
+      default {
+      }
+    }
+  } 
+  return $resultmsg
+}
+
+# This procedure performs variable substitutions on the RUN: lines of a test
+# cases.
+proc substitute { line test tmpFile } {
+  global srcroot objroot srcdir objdir subdir target_triplet prcontext 
+  global llvmgcc llvmgxx llvmgcc_version llvmgccmajvers 
+  global gccpath gxxpath compile_c compile_cxx link shlibext llvmlibsdir
+  global llvmtoolsdir
+  set path [file join $srcdir $subdir]
+
+  # Substitute all Tcl variables.
+  set new_line [subst $line ]
+
+  #replace %prcontext with prcontext.tcl (Must replace before %p)
+  regsub -all {%prcontext} $new_line $prcontext new_line
+  #replace %llvmgcc with actual path to llvmgcc
+  regsub -all {%llvmgcc} $new_line "$llvmgcc -emit-llvm" new_line
+  #replace %llvmgxx with actual path to llvmg++
+  regsub -all {%llvmgxx} $new_line "$llvmgxx -emit-llvm" new_line
+  #replace %compile_c with C compilation command
+  regsub -all {%compile_c} $new_line "$compile_c" new_line
+  #replace %compile_cxx with C++ compilation command
+  regsub -all {%compile_cxx} $new_line "$compile_cxx" new_line
+  #replace %link with C++ link command
+  regsub -all {%link} $new_line "$link" new_line
+  #replace %shlibext with shared library extension
+  regsub -all {%shlibext} $new_line "$shlibext" new_line
+  #replace %llvmlibsdir with configure library directory
+  regsub -all {%llvmlibsdir} $new_line "$llvmlibsdir" new_line
+  #replace %klee with klee binary
+  regsub -all {%klee} $new_line "klee" new_line
+  #replace %kleaver with kleaver binary
+  regsub -all {%kleaver} $new_line "kleaver" new_line
+  #replace %p with path to source, 
+  regsub -all {%p} $new_line [file join $srcdir $subdir] new_line
+  #replace %s with filename
+  regsub -all {%s} $new_line $test new_line
+  #replace %t with temp filenames
+  regsub -all {%t} $new_line $tmpFile new_line
+  #replace %% with %
+  regsub -all {%%} $new_line % new_line
+  return $new_line
+}
+
+# This procedure runs the set of tests for the test_source_files array.
+proc RunLLVMTests { test_source_files } {
+  global srcroot objroot srcdir objdir subdir TEST_FEATURE_LIST target_triplet
+  set timeout 60
+
+  set path [file join $objdir $subdir]
+  
+  #Make Output Directory if it does not exist already
+  if { [file exists path] } {
+    cd $path
+  } else {
+    file mkdir $path
+    cd $path
+  }
+  
+  file mkdir Output
+  cd Output
+
+  foreach test $test_source_files {
+    #Should figure out best way to set the timeout
+    #set timeout 40
+    
+    set filename [file tail $test]
+    set outcome PASS
+    set tmpFile "$filename.tmp"
+
+    #set hasRunline bool to check if testcase has a runline
+    set numLines 0
+
+    # Open the test file and start reading lines
+    set testFileId [ open $test r]
+    set runline ""
+    set PRNUMS ""
+    foreach line [split [read $testFileId] \n] {
+
+      # if its the END. line then stop parsing (optimization for big files)
+      if {[regexp {END.[ *]$} $line match endofscript]} {
+        break
+
+      # if the line is continued, concatenate and continue the loop
+      } elseif {[regexp {RUN: *(.+)(\\)$} $line match oneline suffix]} {
+        set runline "$runline$oneline "
+
+      # if its a terminating RUN: line then do substitution on the whole line
+      # and then save the line.
+      } elseif {[regexp {RUN: *([^&]+)(&&)?} $line match oneline suffix]} {
+        set runline "$runline$oneline"
+        set runline [ substitute $runline $test $tmpFile ]
+        set lines($numLines) $runline
+        set numLines [expr $numLines + 1]
+        set runline ""
+
+      # if its an PR line, save the problem report number
+      } elseif {[regexp {PR([0-9]+)} $line match prnum]} {
+        if {$PRNUMS == ""} {
+          set PRNUMS "PR$prnum"
+        } else {
+          set PRNUMS "$PRNUMS,$prnum"
+        }
+      # if its an XFAIL line, see if we should be XFAILing or not.
+      } elseif {[regexp {XFAIL:[ *](.+)} $line match features]} {
+        set features
+
+        foreach feature [split $features ,] {
+          if { [regexp {\*} $feature match] } {
+              set outcome XFAIL
+          } elseif { [regexp $feature $target_triplet match] } {
+              set outcome XFAIL
+          } elseif { [regexp $feature $TEST_FEATURE_LIST match] } {
+              set outcome XFAIL
+          }
+        }
+      }
+    }
+    
+    # Done reading the script
+    close $testFileId
+    
+    
+    if { $numLines == 0 } {
+      fail "$test: \nDoes not have a RUN line\n"
+    } else {
+      set failed 0
+      for { set i 0 } { $i < $numLines } { set i [ expr $i + 1 ] } {
+        regsub ^.*RUN:(.*) $lines($i) \1 theLine
+        set resultmsg [execOneLine $test $PRNUMS $outcome $i $theLine ]
+        if { $resultmsg != "" } {
+          if { $outcome == "XFAIL" } {
+            xfail "$resultmsg"
+          } else {
+            fail "$resultmsg"
+          }
+          set failed 1
+          break
+        }
+      }
+      if { $failed } {
+        continue
+      } else {
+        if { $PRNUMS != "" } {
+          set PRNUMS " for $PRNUMS"
+        }
+        if { $outcome == "XFAIL" } {
+          xpass "$test$PRNUMS"
+        } else {
+          pass "$test$PRNUMS"
+        }
+      }
+    }
+  }
+}
+
+# Check if klee was configured with POSIX runtime support.
+proc klee_supports_posix_runtime { } {
+    global ENABLE_POSIX_RUNTIME
+    if { $ENABLE_POSIX_RUNTIME == "1" } {
+        return 1
+    }
+    return 0
+}
+
+# Check if klee was configured with uclibc support.
+proc klee_supports_uclibc { } {
+    global ENABLE_UCLIBC
+    if { $ENABLE_UCLIBC == "1" } {
+        return 1
+    }
+    return 0
+}