From bd8cf4ee4d51b6a77c4ce44e2f5cf17eb3458415627a92fb4abf3cc85469130c Mon Sep 17 00:00:00 2001 From: Jiri Slaby Date: Fri, 28 Jun 2024 07:45:50 +0000 Subject: [PATCH] up to 3.1+20240614 OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=140 --- .gitattributes | 23 + .gitignore | 1 + FileCheck.cpp | 895 +++++++++++++++++++ _service | 17 + _servicedata | 4 + klee-3.1+20240614.obscpio | 3 + klee-rpmlintrc | 1 + klee.changes | 1771 +++++++++++++++++++++++++++++++++++++ klee.obsinfo | 4 + klee.spec | 147 +++ not.cpp | 82 ++ 11 files changed, 2948 insertions(+) create mode 100644 .gitattributes create mode 100644 .gitignore create mode 100644 FileCheck.cpp create mode 100644 _service create mode 100644 _servicedata create mode 100644 klee-3.1+20240614.obscpio create mode 100644 klee-rpmlintrc create mode 100644 klee.changes create mode 100644 klee.obsinfo create mode 100644 klee.spec create mode 100644 not.cpp diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..9b03811 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,23 @@ +## Default LFS +*.7z filter=lfs diff=lfs merge=lfs -text +*.bsp filter=lfs diff=lfs merge=lfs -text +*.bz2 filter=lfs diff=lfs merge=lfs -text +*.gem filter=lfs diff=lfs merge=lfs -text +*.gz filter=lfs diff=lfs merge=lfs -text +*.jar filter=lfs diff=lfs merge=lfs -text +*.lz filter=lfs diff=lfs merge=lfs -text +*.lzma filter=lfs diff=lfs merge=lfs -text +*.obscpio filter=lfs diff=lfs merge=lfs -text +*.oxt filter=lfs diff=lfs merge=lfs -text +*.pdf filter=lfs diff=lfs merge=lfs -text +*.png filter=lfs diff=lfs merge=lfs -text +*.rpm filter=lfs diff=lfs merge=lfs -text +*.tbz filter=lfs diff=lfs merge=lfs -text +*.tbz2 filter=lfs diff=lfs merge=lfs -text +*.tgz filter=lfs diff=lfs merge=lfs -text +*.ttf filter=lfs diff=lfs merge=lfs -text +*.txz filter=lfs diff=lfs merge=lfs -text +*.whl filter=lfs diff=lfs merge=lfs -text +*.xz filter=lfs diff=lfs merge=lfs -text +*.zip filter=lfs diff=lfs merge=lfs -text +*.zst filter=lfs diff=lfs merge=lfs -text diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..57affb6 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.osc diff --git a/FileCheck.cpp b/FileCheck.cpp new file mode 100644 index 0000000..00d5240 --- /dev/null +++ b/FileCheck.cpp @@ -0,0 +1,895 @@ +//===- FileCheck.cpp - Check that File's Contents match what is expected --===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// FileCheck does a line-by line check of a file that validates whether it +// contains the expected content. This is useful for regression tests etc. +// +// This program exits with an exit status of 2 on error, exit status of 0 if +// the file matched the expected contents, and exit status of 1 if it did not +// contain the expected contents. +// +//===----------------------------------------------------------------------===// + +#include "llvm/FileCheck/FileCheck.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/InitLLVM.h" +#include "llvm/Support/MemoryBuffer.h" +#include "llvm/Support/Process.h" +#include "llvm/Support/SourceMgr.h" +#include "llvm/Support/WithColor.h" +#include "llvm/Support/raw_ostream.h" +#include +#include +using namespace llvm; + +static cl::extrahelp FileCheckOptsEnv( + "\nOptions are parsed from the environment variable FILECHECK_OPTS and\n" + "from the command line.\n"); + +static cl::opt + CheckFilename(cl::Positional, cl::desc(""), cl::Optional); + +static cl::opt + InputFilename("input-file", cl::desc("File to check (defaults to stdin)"), + cl::init("-"), cl::value_desc("filename")); + +static cl::list CheckPrefixes( + "check-prefix", + cl::desc("Prefix to use from check file (defaults to 'CHECK')")); +static cl::alias CheckPrefixesAlias( + "check-prefixes", cl::aliasopt(CheckPrefixes), cl::CommaSeparated, + cl::NotHidden, + cl::desc( + "Alias for -check-prefix permitting multiple comma separated values")); + +static cl::list CommentPrefixes( + "comment-prefixes", cl::CommaSeparated, cl::Hidden, + cl::desc("Comma-separated list of comment prefixes to use from check file\n" + "(defaults to 'COM,RUN'). Please avoid using this feature in\n" + "LLVM's LIT-based test suites, which should be easier to\n" + "maintain if they all follow a consistent comment style. This\n" + "feature is meant for non-LIT test suites using FileCheck.")); + +static cl::opt NoCanonicalizeWhiteSpace( + "strict-whitespace", + cl::desc("Do not treat all horizontal whitespace as equivalent")); + +static cl::opt IgnoreCase( + "ignore-case", + cl::desc("Use case-insensitive matching")); + +static cl::list ImplicitCheckNot( + "implicit-check-not", + cl::desc("Add an implicit negative check with this pattern to every\n" + "positive check. This can be used to ensure that no instances of\n" + "this pattern occur which are not matched by a positive pattern"), + cl::value_desc("pattern")); + +static cl::list + GlobalDefines("D", cl::AlwaysPrefix, + cl::desc("Define a variable to be used in capture patterns."), + cl::value_desc("VAR=VALUE")); + +static cl::opt AllowEmptyInput( + "allow-empty", cl::init(false), + cl::desc("Allow the input file to be empty. This is useful when making\n" + "checks that some error message does not occur, for example.")); + +static cl::opt AllowUnusedPrefixes( + "allow-unused-prefixes", + cl::desc("Allow prefixes to be specified but not appear in the test.")); + +static cl::opt MatchFullLines( + "match-full-lines", cl::init(false), + cl::desc("Require all positive matches to cover an entire input line.\n" + "Allows leading and trailing whitespace if --strict-whitespace\n" + "is not also passed.")); + +static cl::opt EnableVarScope( + "enable-var-scope", cl::init(false), + cl::desc("Enables scope for regex variables. Variables with names that\n" + "do not start with '$' will be reset at the beginning of\n" + "each CHECK-LABEL block.")); + +static cl::opt AllowDeprecatedDagOverlap( + "allow-deprecated-dag-overlap", cl::init(false), + cl::desc("Enable overlapping among matches in a group of consecutive\n" + "CHECK-DAG directives. This option is deprecated and is only\n" + "provided for convenience as old tests are migrated to the new\n" + "non-overlapping CHECK-DAG implementation.\n")); + +static cl::opt Verbose( + "v", + cl::desc("Print directive pattern matches, or add them to the input dump\n" + "if enabled.\n")); + +static cl::opt VerboseVerbose( + "vv", + cl::desc("Print information helpful in diagnosing internal FileCheck\n" + "issues, or add it to the input dump if enabled. Implies\n" + "-v.\n")); + +// The order of DumpInputValue members affects their precedence, as documented +// for -dump-input below. +enum DumpInputValue { + DumpInputNever, + DumpInputFail, + DumpInputAlways, + DumpInputHelp +}; + +static cl::list DumpInputs( + "dump-input", + cl::desc("Dump input to stderr, adding annotations representing\n" + "currently enabled diagnostics. When there are multiple\n" + "occurrences of this option, the that appears earliest\n" + "in the list below has precedence. The default is 'fail'.\n"), + cl::value_desc("mode"), + cl::values(clEnumValN(DumpInputHelp, "help", "Explain input dump and quit"), + clEnumValN(DumpInputAlways, "always", "Always dump input"), + clEnumValN(DumpInputFail, "fail", "Dump input on failure"), + clEnumValN(DumpInputNever, "never", "Never dump input"))); + +// The order of DumpInputFilterValue members affects their precedence, as +// documented for -dump-input-filter below. +enum DumpInputFilterValue { + DumpInputFilterError, + DumpInputFilterAnnotation, + DumpInputFilterAnnotationFull, + DumpInputFilterAll +}; + +static cl::list DumpInputFilters( + "dump-input-filter", + cl::desc("In the dump requested by -dump-input, print only input lines of\n" + "kind plus any context specified by -dump-input-context.\n" + "When there are multiple occurrences of this option, the \n" + "that appears earliest in the list below has precedence. The\n" + "default is 'error' when -dump-input=fail, and it's 'all' when\n" + "-dump-input=always.\n"), + cl::values(clEnumValN(DumpInputFilterAll, "all", "All input lines"), + clEnumValN(DumpInputFilterAnnotationFull, "annotation-full", + "Input lines with annotations"), + clEnumValN(DumpInputFilterAnnotation, "annotation", + "Input lines with starting points of annotations"), + clEnumValN(DumpInputFilterError, "error", + "Input lines with starting points of error " + "annotations"))); + +static cl::list DumpInputContexts( + "dump-input-context", cl::value_desc("N"), + cl::desc("In the dump requested by -dump-input, print input lines\n" + "before and input lines after any lines specified by\n" + "-dump-input-filter. When there are multiple occurrences of\n" + "this option, the largest specified has precedence. The\n" + "default is 5.\n")); + +typedef cl::list::const_iterator prefix_iterator; + + + + + + + +static void DumpCommandLine(int argc, char **argv) { + errs() << "FileCheck command line: "; + for (int I = 0; I < argc; I++) + errs() << " " << argv[I]; + errs() << "\n"; +} + +struct MarkerStyle { + /// The starting char (before tildes) for marking the line. + char Lead; + /// What color to use for this annotation. + raw_ostream::Colors Color; + /// A note to follow the marker, or empty string if none. + std::string Note; + /// Does this marker indicate inclusion by -dump-input-filter=error? + bool FiltersAsError; + MarkerStyle() {} + MarkerStyle(char Lead, raw_ostream::Colors Color, + const std::string &Note = "", bool FiltersAsError = false) + : Lead(Lead), Color(Color), Note(Note), FiltersAsError(FiltersAsError) { + assert((!FiltersAsError || !Note.empty()) && + "expected error diagnostic to have note"); + } +}; + +static MarkerStyle GetMarker(FileCheckDiag::MatchType MatchTy) { + switch (MatchTy) { + case FileCheckDiag::MatchFoundAndExpected: + return MarkerStyle('^', raw_ostream::GREEN); + case FileCheckDiag::MatchFoundButExcluded: + return MarkerStyle('!', raw_ostream::RED, "error: no match expected", + /*FiltersAsError=*/true); + case FileCheckDiag::MatchFoundButWrongLine: + return MarkerStyle('!', raw_ostream::RED, "error: match on wrong line", + /*FiltersAsError=*/true); + case FileCheckDiag::MatchFoundButDiscarded: + return MarkerStyle('!', raw_ostream::CYAN, + "discard: overlaps earlier match"); + case FileCheckDiag::MatchFoundErrorNote: + // Note should always be overridden within the FileCheckDiag. + return MarkerStyle('!', raw_ostream::RED, + "error: unknown error after match", + /*FiltersAsError=*/true); + case FileCheckDiag::MatchNoneAndExcluded: + return MarkerStyle('X', raw_ostream::GREEN); + case FileCheckDiag::MatchNoneButExpected: + return MarkerStyle('X', raw_ostream::RED, "error: no match found", + /*FiltersAsError=*/true); + case FileCheckDiag::MatchNoneForInvalidPattern: + return MarkerStyle('X', raw_ostream::RED, + "error: match failed for invalid pattern", + /*FiltersAsError=*/true); + case FileCheckDiag::MatchFuzzy: + return MarkerStyle('?', raw_ostream::MAGENTA, "possible intended match", + /*FiltersAsError=*/true); + } + llvm_unreachable_internal("unexpected match type"); +} + +static void DumpInputAnnotationHelp(raw_ostream &OS) { + OS << "The following description was requested by -dump-input=help to\n" + << "explain the input dump printed by FileCheck.\n" + << "\n" + << "Related command-line options:\n" + << "\n" + << " - -dump-input= enables or disables the input dump\n" + << " - -dump-input-filter= filters the input lines\n" + << " - -dump-input-context= adjusts the context of filtered lines\n" + << " - -v and -vv add more annotations\n" + << " - -color forces colors to be enabled both in the dump and below\n" + << " - -help documents the above options in more detail\n" + << "\n" + << "These options can also be set via FILECHECK_OPTS. For example, for\n" + << "maximum debugging output on failures:\n" + << "\n" + << " $ FILECHECK_OPTS='-dump-input-filter=all -vv -color' ninja check\n" + << "\n" + << "Input dump annotation format:\n" + << "\n"; + + // Labels for input lines. + OS << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "L:"; + OS << " labels line number L of the input file\n" + << " An extra space is added after each input line to represent" + << " the\n" + << " newline character\n"; + + // Labels for annotation lines. + OS << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "T:L"; + OS << " labels the only match result for either (1) a pattern of type T" + << " from\n" + << " line L of the check file if L is an integer or (2) the" + << " I-th implicit\n" + << " pattern if L is \"imp\" followed by an integer " + << "I (index origin one)\n"; + OS << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "T:L'N"; + OS << " labels the Nth match result for such a pattern\n"; + + // Markers on annotation lines. + OS << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "^~~"; + OS << " marks good match (reported if -v)\n" + << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "!~~"; + OS << " marks bad match, such as:\n" + << " - CHECK-NEXT on same line as previous match (error)\n" + << " - CHECK-NOT found (error)\n" + << " - CHECK-DAG overlapping match (discarded, reported if " + << "-vv)\n" + << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "X~~"; + OS << " marks search range when no match is found, such as:\n" + << " - CHECK-NEXT not found (error)\n" + << " - CHECK-NOT not found (success, reported if -vv)\n" + << " - CHECK-DAG not found after discarded matches (error)\n" + << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "?"; + OS << " marks fuzzy match when no match is found\n"; + + // Elided lines. + OS << " - "; + WithColor(OS, raw_ostream::SAVEDCOLOR, true) << "..."; + OS << " indicates elided input lines and annotations, as specified by\n" + << " -dump-input-filter and -dump-input-context\n"; + + // Colors. + OS << " - colors "; + WithColor(OS, raw_ostream::GREEN, true) << "success"; + OS << ", "; + WithColor(OS, raw_ostream::RED, true) << "error"; + OS << ", "; + WithColor(OS, raw_ostream::MAGENTA, true) << "fuzzy match"; + OS << ", "; + WithColor(OS, raw_ostream::CYAN, true, false) << "discarded match"; + OS << ", "; + WithColor(OS, raw_ostream::CYAN, true, true) << "unmatched input"; + OS << "\n"; +} + +/// An annotation for a single input line. +struct InputAnnotation { + /// The index of the match result across all checks + unsigned DiagIndex; + /// The label for this annotation. + std::string Label; + /// Is this the initial fragment of a diagnostic that has been broken across + /// multiple lines? + bool IsFirstLine; + /// What input line (one-origin indexing) this annotation marks. This might + /// be different from the starting line of the original diagnostic if + /// !IsFirstLine. + unsigned InputLine; + /// The column range (one-origin indexing, open end) in which to mark the + /// input line. If InputEndCol is UINT_MAX, treat it as the last column + /// before the newline. + unsigned InputStartCol, InputEndCol; + /// The marker to use. + MarkerStyle Marker; + /// Whether this annotation represents a good match for an expected pattern. + bool FoundAndExpectedMatch; +}; + +/// Get an abbreviation for the check type. +static std::string GetCheckTypeAbbreviation(Check::FileCheckType Ty) { + switch (Ty) { + case Check::CheckPlain: + if (Ty.getCount() > 1) + return "count"; + return "check"; + case Check::CheckNext: + return "next"; + case Check::CheckSame: + return "same"; + case Check::CheckNot: + return "not"; + case Check::CheckDAG: + return "dag"; + case Check::CheckLabel: + return "label"; + case Check::CheckEmpty: + return "empty"; + case Check::CheckComment: + return "com"; + case Check::CheckEOF: + return "eof"; + case Check::CheckBadNot: + return "bad-not"; + case Check::CheckBadCount: + return "bad-count"; + case Check::CheckMisspelled: + return "misspelled"; + case Check::CheckNone: + llvm_unreachable("invalid FileCheckType"); + } + llvm_unreachable("unknown FileCheckType"); +} + +static void +BuildInputAnnotations(const SourceMgr &SM, unsigned CheckFileBufferID, + const std::pair &ImpPatBufferIDRange, + const std::vector &Diags, + std::vector &Annotations, + unsigned &LabelWidth) { + struct CompareSMLoc { + bool operator()(const SMLoc &LHS, const SMLoc &RHS) const { + return LHS.getPointer() < RHS.getPointer(); + } + }; + // How many diagnostics does each pattern have? + std::map DiagCountPerPattern; + for (auto Diag : Diags) + ++DiagCountPerPattern[Diag.CheckLoc]; + // How many diagnostics have we seen so far per pattern? + std::map DiagIndexPerPattern; + // How many total diagnostics have we seen so far? + unsigned DiagIndex = 0; + // What's the widest label? + LabelWidth = 0; + for (auto DiagItr = Diags.begin(), DiagEnd = Diags.end(); DiagItr != DiagEnd; + ++DiagItr) { + InputAnnotation A; + A.DiagIndex = DiagIndex++; + + // Build label, which uniquely identifies this check result. + unsigned CheckBufferID = SM.FindBufferContainingLoc(DiagItr->CheckLoc); + auto CheckLineAndCol = + SM.getLineAndColumn(DiagItr->CheckLoc, CheckBufferID); + llvm::raw_string_ostream Label(A.Label); + Label << GetCheckTypeAbbreviation(DiagItr->CheckTy) << ":"; + if (CheckBufferID == CheckFileBufferID) + Label << CheckLineAndCol.first; + else if (ImpPatBufferIDRange.first <= CheckBufferID && + CheckBufferID < ImpPatBufferIDRange.second) + Label << "imp" << (CheckBufferID - ImpPatBufferIDRange.first + 1); + else + llvm_unreachable("expected diagnostic's check location to be either in " + "the check file or for an implicit pattern"); + if (DiagCountPerPattern[DiagItr->CheckLoc] > 1) + Label << "'" << DiagIndexPerPattern[DiagItr->CheckLoc]++; + LabelWidth = std::max((std::string::size_type)LabelWidth, A.Label.size()); + + A.Marker = GetMarker(DiagItr->MatchTy); + if (!DiagItr->Note.empty()) { + A.Marker.Note = DiagItr->Note; + // It's less confusing if notes that don't actually have ranges don't have + // markers. For example, a marker for 'with "VAR" equal to "5"' would + // seem to indicate where "VAR" matches, but the location we actually have + // for the marker simply points to the start of the match/search range for + // the full pattern of which the substitution is potentially just one + // component. + if (DiagItr->InputStartLine == DiagItr->InputEndLine && + DiagItr->InputStartCol == DiagItr->InputEndCol) + A.Marker.Lead = ' '; + } + if (DiagItr->MatchTy == FileCheckDiag::MatchFoundErrorNote) { + assert(!DiagItr->Note.empty() && + "expected custom note for MatchFoundErrorNote"); + A.Marker.Note = "error: " + A.Marker.Note; + } + A.FoundAndExpectedMatch = + DiagItr->MatchTy == FileCheckDiag::MatchFoundAndExpected; + + // Compute the mark location, and break annotation into multiple + // annotations if it spans multiple lines. + A.IsFirstLine = true; + A.InputLine = DiagItr->InputStartLine; + A.InputStartCol = DiagItr->InputStartCol; + if (DiagItr->InputStartLine == DiagItr->InputEndLine) { + // Sometimes ranges are empty in order to indicate a specific point, but + // that would mean nothing would be marked, so adjust the range to + // include the following character. + A.InputEndCol = + std::max(DiagItr->InputStartCol + 1, DiagItr->InputEndCol); + Annotations.push_back(A); + } else { + assert(DiagItr->InputStartLine < DiagItr->InputEndLine && + "expected input range not to be inverted"); + A.InputEndCol = UINT_MAX; + Annotations.push_back(A); + for (unsigned L = DiagItr->InputStartLine + 1, E = DiagItr->InputEndLine; + L <= E; ++L) { + // If a range ends before the first column on a line, then it has no + // characters on that line, so there's nothing to render. + if (DiagItr->InputEndCol == 1 && L == E) + break; + InputAnnotation B; + B.DiagIndex = A.DiagIndex; + B.Label = A.Label; + B.IsFirstLine = false; + B.InputLine = L; + B.Marker = A.Marker; + B.Marker.Lead = '~'; + B.Marker.Note = ""; + B.InputStartCol = 1; + if (L != E) + B.InputEndCol = UINT_MAX; + else + B.InputEndCol = DiagItr->InputEndCol; + B.FoundAndExpectedMatch = A.FoundAndExpectedMatch; + Annotations.push_back(B); + } + } + } +} + +static unsigned FindInputLineInFilter( + DumpInputFilterValue DumpInputFilter, unsigned CurInputLine, + const std::vector::iterator &AnnotationBeg, + const std::vector::iterator &AnnotationEnd) { + if (DumpInputFilter == DumpInputFilterAll) + return CurInputLine; + for (auto AnnotationItr = AnnotationBeg; AnnotationItr != AnnotationEnd; + ++AnnotationItr) { + switch (DumpInputFilter) { + case DumpInputFilterAll: + llvm_unreachable("unexpected DumpInputFilterAll"); + break; + case DumpInputFilterAnnotationFull: + return AnnotationItr->InputLine; + case DumpInputFilterAnnotation: + if (AnnotationItr->IsFirstLine) + return AnnotationItr->InputLine; + break; + case DumpInputFilterError: + if (AnnotationItr->IsFirstLine && AnnotationItr->Marker.FiltersAsError) + return AnnotationItr->InputLine; + break; + } + } + return UINT_MAX; +} + +/// To OS, print a vertical ellipsis (right-justified at LabelWidth) if it would +/// occupy less lines than ElidedLines, but print ElidedLines otherwise. Either +/// way, clear ElidedLines. Thus, if ElidedLines is empty, do nothing. +static void DumpEllipsisOrElidedLines(raw_ostream &OS, std::string &ElidedLines, + unsigned LabelWidth) { + if (ElidedLines.empty()) + return; + unsigned EllipsisLines = 3; + if (EllipsisLines < StringRef(ElidedLines).count('\n')) { + for (unsigned i = 0; i < EllipsisLines; ++i) { + WithColor(OS, raw_ostream::BLACK, /*Bold=*/true) + << right_justify(".", LabelWidth); + OS << '\n'; + } + } else + OS << ElidedLines; + ElidedLines.clear(); +} + +static void DumpAnnotatedInput(raw_ostream &OS, const FileCheckRequest &Req, + DumpInputFilterValue DumpInputFilter, + unsigned DumpInputContext, + StringRef InputFileText, + std::vector &Annotations, + unsigned LabelWidth) { + OS << "Input was:\n<<<<<<\n"; + + // Sort annotations. + llvm::sort(Annotations, + [](const InputAnnotation &A, const InputAnnotation &B) { + // 1. Sort annotations in the order of the input lines. + // + // This makes it easier to find relevant annotations while + // iterating input lines in the implementation below. FileCheck + // does not always produce diagnostics in the order of input + // lines due to, for example, CHECK-DAG and CHECK-NOT. + if (A.InputLine != B.InputLine) + return A.InputLine < B.InputLine; + // 2. Sort annotations in the temporal order FileCheck produced + // their associated diagnostics. + // + // This sort offers several benefits: + // + // A. On a single input line, the order of annotations reflects + // the FileCheck logic for processing directives/patterns. + // This can be helpful in understanding cases in which the + // order of the associated directives/patterns in the check + // file or on the command line either (i) does not match the + // temporal order in which FileCheck looks for matches for the + // directives/patterns (due to, for example, CHECK-LABEL, + // CHECK-NOT, or `--implicit-check-not`) or (ii) does match + // that order but does not match the order of those + // diagnostics along an input line (due to, for example, + // CHECK-DAG). + // + // On the other hand, because our presentation format presents + // input lines in order, there's no clear way to offer the + // same benefit across input lines. For consistency, it might + // then seem worthwhile to have annotations on a single line + // also sorted in input order (that is, by input column). + // However, in practice, this appears to be more confusing + // than helpful. Perhaps it's intuitive to expect annotations + // to be listed in the temporal order in which they were + // produced except in cases the presentation format obviously + // and inherently cannot support it (that is, across input + // lines). + // + // B. When diagnostics' annotations are split among multiple + // input lines, the user must track them from one input line + // to the next. One property of the sort chosen here is that + // it facilitates the user in this regard by ensuring the + // following: when comparing any two input lines, a + // diagnostic's annotations are sorted in the same position + // relative to all other diagnostics' annotations. + return A.DiagIndex < B.DiagIndex; + }); + + // Compute the width of the label column. + const unsigned char *InputFilePtr = InputFileText.bytes_begin(), + *InputFileEnd = InputFileText.bytes_end(); + unsigned LineCount = InputFileText.count('\n'); + if (InputFileEnd[-1] != '\n') + ++LineCount; + unsigned LineNoWidth = std::log10(LineCount) + 1; + // +3 below adds spaces (1) to the left of the (right-aligned) line numbers + // on input lines and (2) to the right of the (left-aligned) labels on + // annotation lines so that input lines and annotation lines are more + // visually distinct. For example, the spaces on the annotation lines ensure + // that input line numbers and check directive line numbers never align + // horizontally. Those line numbers might not even be for the same file. + // One space would be enough to achieve that, but more makes it even easier + // to see. + LabelWidth = std::max(LabelWidth, LineNoWidth) + 3; + + // Print annotated input lines. + unsigned PrevLineInFilter = 0; // 0 means none so far + unsigned NextLineInFilter = 0; // 0 means uncomputed, UINT_MAX means none + std::string ElidedLines; + raw_string_ostream ElidedLinesOS(ElidedLines); + ColorMode TheColorMode = + WithColor(OS).colorsEnabled() ? ColorMode::Enable : ColorMode::Disable; + if (TheColorMode == ColorMode::Enable) + ElidedLinesOS.enable_colors(true); + auto AnnotationItr = Annotations.begin(), AnnotationEnd = Annotations.end(); + for (unsigned Line = 1; + InputFilePtr != InputFileEnd || AnnotationItr != AnnotationEnd; + ++Line) { + const unsigned char *InputFileLine = InputFilePtr; + + // Compute the previous and next line included by the filter. + if (NextLineInFilter < Line) + NextLineInFilter = FindInputLineInFilter(DumpInputFilter, Line, + AnnotationItr, AnnotationEnd); + assert(NextLineInFilter && "expected NextLineInFilter to be computed"); + if (NextLineInFilter == Line) + PrevLineInFilter = Line; + + // Elide this input line and its annotations if it's not within the + // context specified by -dump-input-context of an input line included by + // -dump-input-filter. However, in case the resulting ellipsis would occupy + // more lines than the input lines and annotations it elides, buffer the + // elided lines and annotations so we can print them instead. + raw_ostream *LineOS; + if ((!PrevLineInFilter || PrevLineInFilter + DumpInputContext < Line) && + (NextLineInFilter == UINT_MAX || + Line + DumpInputContext < NextLineInFilter)) + LineOS = &ElidedLinesOS; + else { + LineOS = &OS; + DumpEllipsisOrElidedLines(OS, ElidedLinesOS.str(), LabelWidth); + } + + // Print right-aligned line number. + WithColor(*LineOS, raw_ostream::BLACK, /*Bold=*/true, /*BF=*/false, + TheColorMode) + << format_decimal(Line, LabelWidth) << ": "; + + // For the case where -v and colors are enabled, find the annotations for + // good matches for expected patterns in order to highlight everything + // else in the line. There are no such annotations if -v is disabled. + std::vector FoundAndExpectedMatches; + if (Req.Verbose && TheColorMode == ColorMode::Enable) { + for (auto I = AnnotationItr; I != AnnotationEnd && I->InputLine == Line; + ++I) { + if (I->FoundAndExpectedMatch) + FoundAndExpectedMatches.push_back(*I); + } + } + + // Print numbered line with highlighting where there are no matches for + // expected patterns. + bool Newline = false; + { + WithColor COS(*LineOS, raw_ostream::SAVEDCOLOR, /*Bold=*/false, + /*BG=*/false, TheColorMode); + bool InMatch = false; + if (Req.Verbose) + COS.changeColor(raw_ostream::CYAN, true, true); + for (unsigned Col = 1; InputFilePtr != InputFileEnd && !Newline; ++Col) { + bool WasInMatch = InMatch; + InMatch = false; + for (auto M : FoundAndExpectedMatches) { + if (M.InputStartCol <= Col && Col < M.InputEndCol) { + InMatch = true; + break; + } + } + if (!WasInMatch && InMatch) + COS.resetColor(); + else if (WasInMatch && !InMatch) + COS.changeColor(raw_ostream::CYAN, true, true); + if (*InputFilePtr == '\n') { + Newline = true; + COS << ' '; + } else + COS << *InputFilePtr; + ++InputFilePtr; + } + } + *LineOS << '\n'; + unsigned InputLineWidth = InputFilePtr - InputFileLine; + + // Print any annotations. + while (AnnotationItr != AnnotationEnd && + AnnotationItr->InputLine == Line) { + WithColor COS(*LineOS, AnnotationItr->Marker.Color, /*Bold=*/true, + /*BG=*/false, TheColorMode); + // The two spaces below are where the ": " appears on input lines. + COS << left_justify(AnnotationItr->Label, LabelWidth) << " "; + unsigned Col; + for (Col = 1; Col < AnnotationItr->InputStartCol; ++Col) + COS << ' '; + COS << AnnotationItr->Marker.Lead; + // If InputEndCol=UINT_MAX, stop at InputLineWidth. + for (++Col; Col < AnnotationItr->InputEndCol && Col <= InputLineWidth; + ++Col) + COS << '~'; + const std::string &Note = AnnotationItr->Marker.Note; + if (!Note.empty()) { + // Put the note at the end of the input line. If we were to instead + // put the note right after the marker, subsequent annotations for the + // same input line might appear to mark this note instead of the input + // line. + for (; Col <= InputLineWidth; ++Col) + COS << ' '; + COS << ' ' << Note; + } + COS << '\n'; + ++AnnotationItr; + } + } + DumpEllipsisOrElidedLines(OS, ElidedLinesOS.str(), LabelWidth); + + OS << ">>>>>>\n"; +} + +int main(int argc, char **argv) { + // Enable use of ANSI color codes because FileCheck is using them to + // highlight text. + llvm::sys::Process::UseANSIEscapeCodes(true); + + InitLLVM X(argc, argv); + cl::ParseCommandLineOptions(argc, argv, /*Overview*/ "", /*Errs*/ nullptr, + "FILECHECK_OPTS"); + + // Select -dump-input* values. The -help documentation specifies the default + // value and which value to choose if an option is specified multiple times. + // In the latter case, the general rule of thumb is to choose the value that + // provides the most information. + DumpInputValue DumpInput = + DumpInputs.empty() + ? DumpInputFail + : *std::max_element(DumpInputs.begin(), DumpInputs.end()); + DumpInputFilterValue DumpInputFilter; + if (DumpInputFilters.empty()) + DumpInputFilter = DumpInput == DumpInputAlways ? DumpInputFilterAll + : DumpInputFilterError; + else + DumpInputFilter = + *std::max_element(DumpInputFilters.begin(), DumpInputFilters.end()); + unsigned DumpInputContext = DumpInputContexts.empty() + ? 5 + : *std::max_element(DumpInputContexts.begin(), + DumpInputContexts.end()); + + if (DumpInput == DumpInputHelp) { + DumpInputAnnotationHelp(outs()); + return 0; + } + if (CheckFilename.empty()) { + errs() << " not specified\n"; + return 2; + } + + FileCheckRequest Req; + append_range(Req.CheckPrefixes, CheckPrefixes); + + append_range(Req.CommentPrefixes, CommentPrefixes); + + append_range(Req.ImplicitCheckNot, ImplicitCheckNot); + + bool GlobalDefineError = false; + for (StringRef G : GlobalDefines) { + size_t EqIdx = G.find('='); + if (EqIdx == std::string::npos) { + errs() << "Missing equal sign in command-line definition '-D" << G + << "'\n"; + GlobalDefineError = true; + continue; + } + if (EqIdx == 0) { + errs() << "Missing variable name in command-line definition '-D" << G + << "'\n"; + GlobalDefineError = true; + continue; + } + Req.GlobalDefines.push_back(G); + } + if (GlobalDefineError) + return 2; + + Req.AllowEmptyInput = AllowEmptyInput; + Req.AllowUnusedPrefixes = AllowUnusedPrefixes; + Req.EnableVarScope = EnableVarScope; + Req.AllowDeprecatedDagOverlap = AllowDeprecatedDagOverlap; + Req.Verbose = Verbose; + Req.VerboseVerbose = VerboseVerbose; + Req.NoCanonicalizeWhiteSpace = NoCanonicalizeWhiteSpace; + Req.MatchFullLines = MatchFullLines; + Req.IgnoreCase = IgnoreCase; + + if (VerboseVerbose) + Req.Verbose = true; + + FileCheck FC(Req); + if (!FC.ValidateCheckPrefixes()) + return 2; + + Regex PrefixRE = FC.buildCheckPrefixRegex(); + std::string REError; + if (!PrefixRE.isValid(REError)) { + errs() << "Unable to combine check-prefix strings into a prefix regular " + "expression! This is likely a bug in FileCheck's verification of " + "the check-prefix strings. Regular expression parsing failed " + "with the following error: " + << REError << "\n"; + return 2; + } + + SourceMgr SM; + + // Read the expected strings from the check file. + ErrorOr> CheckFileOrErr = + MemoryBuffer::getFileOrSTDIN(CheckFilename, /*IsText=*/true); + if (std::error_code EC = CheckFileOrErr.getError()) { + errs() << "Could not open check file '" << CheckFilename + << "': " << EC.message() << '\n'; + return 2; + } + MemoryBuffer &CheckFile = *CheckFileOrErr.get(); + + SmallString<4096> CheckFileBuffer; + StringRef CheckFileText = FC.CanonicalizeFile(CheckFile, CheckFileBuffer); + + unsigned CheckFileBufferID = + SM.AddNewSourceBuffer(MemoryBuffer::getMemBuffer( + CheckFileText, CheckFile.getBufferIdentifier()), + SMLoc()); + + std::pair ImpPatBufferIDRange; + if (FC.readCheckFile(SM, CheckFileText, PrefixRE, &ImpPatBufferIDRange)) + return 2; + + // Open the file to check and add it to SourceMgr. + ErrorOr> InputFileOrErr = + MemoryBuffer::getFileOrSTDIN(InputFilename, /*IsText=*/true); + if (InputFilename == "-") + InputFilename = ""; // Overwrite for improved diagnostic messages + if (std::error_code EC = InputFileOrErr.getError()) { + errs() << "Could not open input file '" << InputFilename + << "': " << EC.message() << '\n'; + return 2; + } + MemoryBuffer &InputFile = *InputFileOrErr.get(); + + if (InputFile.getBufferSize() == 0 && !AllowEmptyInput) { + errs() << "FileCheck error: '" << InputFilename << "' is empty.\n"; + DumpCommandLine(argc, argv); + return 2; + } + + SmallString<4096> InputFileBuffer; + StringRef InputFileText = FC.CanonicalizeFile(InputFile, InputFileBuffer); + + SM.AddNewSourceBuffer(MemoryBuffer::getMemBuffer( + InputFileText, InputFile.getBufferIdentifier()), + SMLoc()); + + std::vector Diags; + int ExitCode = FC.checkInput(SM, InputFileText, + DumpInput == DumpInputNever ? nullptr : &Diags) + ? EXIT_SUCCESS + : 1; + if (DumpInput == DumpInputAlways || + (ExitCode == 1 && DumpInput == DumpInputFail)) { + errs() << "\n" + << "Input file: " << InputFilename << "\n" + << "Check file: " << CheckFilename << "\n" + << "\n" + << "-dump-input=help explains the following input dump.\n" + << "\n"; + std::vector Annotations; + unsigned LabelWidth; + BuildInputAnnotations(SM, CheckFileBufferID, ImpPatBufferIDRange, Diags, + Annotations, LabelWidth); + DumpAnnotatedInput(errs(), Req, DumpInputFilter, DumpInputContext, + InputFileText, Annotations, LabelWidth); + } + + return ExitCode; +} diff --git a/_service b/_service new file mode 100644 index 0000000..4226c40 --- /dev/null +++ b/_service @@ -0,0 +1,17 @@ + + + https://github.com/klee/klee + git + enable + @PARENT_TAG@+%cd + v(.*) + \1 + + + + + + klee-*.tar + xz + + diff --git a/_servicedata b/_servicedata new file mode 100644 index 0000000..07e0302 --- /dev/null +++ b/_servicedata @@ -0,0 +1,4 @@ + + + https://github.com/klee/klee + 26632f1d883e1343a23fd200d2dde070707b294d \ No newline at end of file diff --git a/klee-3.1+20240614.obscpio b/klee-3.1+20240614.obscpio new file mode 100644 index 0000000..bb708e1 --- /dev/null +++ b/klee-3.1+20240614.obscpio @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:88dc7191d257300ef08e5eb58b72860f1c1b65a8f93da57ece4393b024164856 +size 19195405 diff --git a/klee-rpmlintrc b/klee-rpmlintrc new file mode 100644 index 0000000..67d25fd --- /dev/null +++ b/klee-rpmlintrc @@ -0,0 +1 @@ +addFilter("devel-file-in-non-devel-package") diff --git a/klee.changes b/klee.changes new file mode 100644 index 0000000..1bf52b0 --- /dev/null +++ b/klee.changes @@ -0,0 +1,1771 @@ +------------------------------------------------------------------- +Fri Jun 28 07:39:18 UTC 2024 - jslaby@suse.cz + +- Update to version 3.1+20240614: + * Mark variadic argument tests as requiring x86_64 + * Mark inline assembly tests as requiring x86_64 + * Add handler for _Exit(3) + +------------------------------------------------------------------- +Thu Apr 25 06:08:03 UTC 2024 - jslaby@suse.cz + +- Update to version 3.1+20240418: + * Renamed test/Expr to test/kleaver and move ReadExprConsistency.c to + test/Feature + * Workaround for MSan failures due to + https://github.com/llvm/llvm-project/issues/78354 + * Addressed missing override warnings emitted by recent compilers + * add pythonpath to lit forwarded env vars + * TARGET_TRIPLE was renamed to LLVM_TARGET_TRIPLE since LLVM 15 + * New domain name klee-se.org, updating links. + * Final changes to release notes for v3.1 + * Add support to fully concretise objects if modified externally + * Support external call concretisation policies for referenced objects + * Refactor `ObjectState::flushToConcreteStore` to use `toConstant` + * Use correctly constrained constants if the memory object is fully symbolic + * Correctly update symbolic variables that have been changed externally + * and much more. +- Remove + * 0001-Fix-brittleness-in-Feature-VarArgByVal-test.patch (in upstream) + +------------------------------------------------------------------- +Fri Feb 09 07:40:49 UTC 2024 - jslaby@suse.cz + +- Update to version 3.0+20240208: + * Add space between include and main function for updated test cases + * Mention default value in help text for `--strip-all` and `--strip-debug` + * Use `std::` namespace for `uint64_t` + * Enable CI to test newer LLVM versions + * Support newer LLVM versions in `lit` + * Update test case for expressions using `udiv`, `urem`, `sdiv` and `srem` + * Handle check for thrown libc++ exceptions more general + * Disable `2018-10-30-llvm-pr39177.ll` for newer LLVM versions. + * Disable unsupported passes for newer LLVM versions + * Add support to `aligned_alloc` generated by LLVM + * Add support for `Intrinsic::get_rounding` for LLVM 16 + * Use APIs of newer LLVM versions instead of unsupported ones + * Fix test case: using unsupported `CHECK_NEXT` instead of `CHECK-NEXT` + * Fix test cases to support opaque pointers + * Add support for opaque pointers + * Explicitly enable opaque pointer support for LLVM 15 + * Explicitly build KLEE's exception handling runtime with C++11 + * Assume C compiler's default standard is `-std=gnu17` + * Use KLEE's uClibc v1.4 as default to support the compilation with newer compilers + * Refactor invocation of old pass manager into legacy function +- remove (they were upstreamed) + * 0001-Add-support-to-build-newer-LLVM-versions.patch + * 0002-Add-support-for-newer-libc-Simplify-path-detection.patch + * 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch + * 0004-Fix-klee-libc-memchr.c-compiler-warning.patch + * 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch + * 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch + * 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch + * 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch + * 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch + * 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch + * 0011-Add-support-for-opaque-pointers.patch + * 0012-Fix-test-cases-to-support-opaque-pointers.patch + * 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch + * 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch + * 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch + * 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch + * 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch + * 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch + * 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch + * 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch + * 0021-Support-newer-LLVM-versions-in-lit.patch + * 0022-Enable-CI-to-test-newer-LLVM-versions.patch +- remove 0001-test-disable-failing-tests-with-llvm-15.patch + Fixed by the below patch (in a PR), and in klee-uclibc. +- add + * 0001-Fix-brittleness-in-Feature-VarArgByVal-test.patch + +------------------------------------------------------------------- +Thu Dec 14 07:40:13 UTC 2023 - jslaby@suse.cz + +- Update to version 3.0+20231023: + * replace deprecated (as of c++20) std::is_pod with std::trivial && + std::is_standard_layout + * Make KDAlloc the default memory allocator + * Remove broken experimental optimisation for validity (--cex-cache-exp) + * Add code to only keep in the --help menu the KLEE/Kleaver option categories + * Move some options to the klee namespace and declare them in + OptionCategories.h + * Replaced --suppress-external-warnings and --all-external-warnings with + --external-call-warnings=none|once-per-function|all. + * Combine all `ConstantExpr::toMemory` cases into one. + * Using std::memcpy prevents alignment problems and removes an unnecessary + special case + * Implement getLocationInfo in the same style as getSize + * Have CoWPtr::get and CoWPtr::getOwned return pointers instead of references + * rename Allocator::location_info to Allocator::locationInfo for consistency + * Consistently use ".ktest" when referring to .ktest files in the help menu + * Remove parentheses around klee_ intrinsics from the help menu + * Fixed a couple of spelling issues in the help menu + * Improved help message for --exit-on-error-type=Abort + * and more +- clean up spec file and switch to manual service +- switch to LLVM 16 +- added patches + * 0001-Add-support-to-build-newer-LLVM-versions.patch + * 0001-test-disable-failing-tests-with-llvm-15.patch + * 0002-Add-support-for-newer-libc-Simplify-path-detection.patch + * 0003-Replace-libcxx_include-with-libcxx_includes-for-mult.patch + * 0004-Fix-klee-libc-memchr.c-compiler-warning.patch + * 0005-Fix-klee_eh_cxx.cpp-compiler-error.patch + * 0006-Refactor-invocation-of-old-pass-manager-into-legacy-.patch + * 0007-Use-KLEE-s-uClibc-v1.4-as-default-to-support-the-com.patch + * 0008-Assume-C-compiler-s-default-standard-is-std-gnu17.patch + * 0009-Explicitly-build-KLEE-s-exception-handling-runtime-w.patch + * 0010-Explicitly-enable-opaque-pointer-support-for-LLVM-15.patch + * 0011-Add-support-for-opaque-pointers.patch + * 0012-Fix-test-cases-to-support-opaque-pointers.patch + * 0013-Fix-test-case-using-unsupported-CHECK_NEXT-instead-o.patch + * 0014-Use-APIs-of-newer-LLVM-versions-instead-of-unsupport.patch + * 0015-Add-support-for-Intrinsic-get_rounding-for-LLVM-16.patch + * 0016-Add-support-to-aligned_alloc-generated-by-LLVM.patch + * 0017-Disable-unsupported-passes-for-newer-LLVM-versions.patch + * 0018-Disable-2018-10-30-llvm-pr39177.ll-for-newer-LLVM-ve.patch + * 0019-Handle-check-for-thrown-libc-exceptions-more-general.patch + * 0020-Update-test-case-for-expressions-using-udiv-urem-sdi.patch + * 0021-Support-newer-LLVM-versions-in-lit.patch + * 0022-Enable-CI-to-test-newer-LLVM-versions.patch +- removed patches + * 0001-test-disable-until-it-is-fixed.patch (appears to be unnecessary now) + +------------------------------------------------------------------- +Thu Jun 15 06:54:19 UTC 2023 - jslaby@suse.cz + +- Update to version 3.0+20230611: + * Rewrote has_permission in the POSIX runtime. + * SpecialFunctionHandler: use std::array for handlerInfo + * fix ktest-randgen: use after free + * Fixed a format specifier pointed to by a compiler warning. + * Build and push Docker image as part of a release + * Use recommended LLVM 13 as part of the Docker image + * ktest-gen: remove unused function + * Further improve KDAlloc memory usage with infinite quarantine + * test/Feature/StackTraceOutput.c: relative checks, clang-format + * re-enable StackTraceOutput.c test + * make BatchingSearcher more readable + * fix BatchingSearcher's disabled time budget + * also check for default CHECK directive in ArrayOpt Tests + * CMake: use check_c_source_compiles() for FSTATAT_PATH_ACCEPTS_NULL + * config.h: include FSTATAT_PATH_ACCEPTS_NULL + * doxygen.cfg.in: DOXYGEN_OUTPUT_DIR + * and much more +- remove + * 0001-gcc13-include-cstint-for-int-_t.patch (in upstream) + +------------------------------------------------------------------- +Mon Mar 27 10:31:57 UTC 2023 - jslaby@suse.cz + +- Update to version 2.3+20230326: + * tests: add some missing headers + * fix unused variables warning + * Remove model_version from the POSIX runtime, as we have never used it. + * tests: add some + * stats: add some + * remove obsolete header + * Run KDAlloc/rusage unittest a few times to allow for swapfile interference + * Added more test cases for --entry-point. EntryPointMissing is currently expected to fail. + * STP: add option to switch SAT solver: --stp-sat-solver and set default to CryptoMinisat + * Change `llvm_map_components_to_libnames` to `llvm_config` CMake function + * use C++17 + * Require minimal version of CMake 3.16 for KLEE + * Remove hard to understand and debug pcregrep test + * klee-stats: improve error message for missing tabulate package + * Handle fail of KLEE gracefully + * Explicitly check if 32bit support is enabled for testing +- remove + * 0001-cmake-implement-USE_MAP-to-support-single-LLVM-libra.patch + It's in upstream in a different form. + +------------------------------------------------------------------- +Wed Mar 22 08:17:59 UTC 2023 - jslaby@suse.cz + +- Update to version 2.3+20230320: + * ConstantArrayExprVisitor: Fix detection of multiple array indices + * ConstantArrayExprVisitor: Deduplicate `visitConcat` and `visitRead` + * llvm14 support + * Update KDAlloc unittests + * Don't fail `KleeStats.c` test if it takes 1s or longer + * Disable `const_array_opt1` for ubsan as well + * Fix uninitialised memory access while reading last path entry + * Fix building of runtime library and klee-replay + * Add support to disable memsan instrumentation; update UB/Asan suppression + * [MemSan] Mark memory objects modified by syscalls as initialised + * Fix compiler warning with newer compilers + * Use bitcode library paths via config generation instead of `-D` flags + * [cmake] Use LLVM's CMake functionality only + * Fixed a bug in KLEE libc's implementation of strcmp: according to the C standard, characters should be compared as unsigned chars. + * Add some system tests for KDAlloc + * Integrate KDAlloc into KLEE + * Have the STP coverage build also provide Z3, so that the crosscheck solver can also be tested + * Add a few simple solver tests + * create klee-last as a relative link + * Fix integer overflow + * Add an extra check to test/Runtime/FreeStanding/memcpy_chk_err.c ensuring that a call to __memcpy_chk is emitted + * fix output check in test const_arr_opt1 + * add missing FileCheck command to test + * Fixed some leaks in klee-replay + * fix FileCheck cmd of VarArgByVal test +- remove (upstream): + * 0001-Module-InstructionOperandTypeCheckPass-Fix-Wbitwise-.patch + * 0001-llvm14-Add-LLVM-14-to-lit.cfg.patch + * 0002-llvm14-TargetRegistry.h-was-moved-from-Support-to-MC.patch + * 0003-llvm14-PointerType-getElementType-was-deprecated.patch +- add + * 0001-cmake-implement-USE_MAP-to-support-single-LLVM-libra.patch + * 0001-gcc13-include-cstint-for-int-_t.patch + +------------------------------------------------------------------- +Tue Oct 25 06:53:25 UTC 2022 - jslaby@suse.cz + +- Update to version 2.3+20220926: + * Improve the message for when large arrays become symbolic. + * Pass llvm.experimental.noalias.scope.decl to IntrinsicLowering so that + it strips out these intrinsics + * Improve pattern for FileCheck in UBSan's tests + * Add README to UBSan runtime + * Eliminate .undefined_behavior.err category and simplify tests + * Check extensions of generated files in tests + * Introduce separate categories for different kinds of undefined behavior + * Support UBSan-enabled binaries +- update FileCheck.cpp to llvm 14's + +------------------------------------------------------------------- +Tue Sep 6 09:21:23 UTC 2022 - Jiri Slaby + +- add llvm 14 support + * 0001-llvm14-Add-LLVM-14-to-lit.cfg.patch + * 0001-Module-InstructionOperandTypeCheckPass-Fix-Wbitwise-.patch + * 0002-llvm14-TargetRegistry.h-was-moved-from-Support-to-MC.patch + * 0003-llvm14-PointerType-getElementType-was-deprecated.patch +- switch to llvm 14 + +------------------------------------------------------------------- +Mon Sep 05 09:12:26 UTC 2022 - jslaby@suse.cz + +- Update to version 2.3+20220826: + * Use true instead of Z3_TRUE (removed in z3 4.11.0) + * Corrected wrong usage of klee_report_error in __cxa_atexit handler + * Support arguments of width 128, 256 and 512 bits for external calls + * POSIX runtime: fstatat: check for nonnull path APIs + * Inline asm external call + * Fix memory leak in crosscheck core solver mechanism + * checkout KLEE with depth > 1 when running codecov + * rename CallSite to CallBase + * remove LLVM < 9 + * Perform coverage analysis for z3 as well + * Remove the CI target metaSMT(Boolector). metaSMT(STP) already runs the + test suite with all solvers supported by metaSMT, so the extra target + provides marginal benefits. + * Implement getArrayForUpdate iteratively + * Fix error with empty EntryPoint + * Intrinsics: Add support for @llvm.f{ma,muladd}.f* + * Use `klee` user to install system dependencies + * Spelling Fixes + * tests: add StackTraceOutput.c + * .err files: minor readability changes to stack trace output + * Update SpecialFunctionHandler.cpp + * tests: invoke LLVM tools through their corresponding macros + +------------------------------------------------------------------- +Tue May 10 09:23:08 UTC 2022 - jslaby@suse.cz + +- Update to version 2.3+20220506: + * Switch to newer KLEE uClibc release + * Updated tests to use ktest-randgen instead of gen-random-bout + * Renamed gen-random-bout to ktest-randgen + * Updated tests to use ktest-gen instead of gen-bout + * Updated klee-zesti to use ktest-gen instead of gen-bout + * Renamed gen-bout to ktest-gen + * cl flags: document default values, remove dead option: + --replay-keep-symbolic + * Make Uclibc support a runtime option, not a compile-time one. + * use mallinfo2 if available + * Remove unnecessary call to deprecated function sqlite3_enable_shared_cache + * Add LLVM 9 and LLVM 11 patches to build with newer Linux kernel versions + * Build libcxx in parallel if possible + * Clearly separate between LLVM, a bitcode compiler, and sanitizer compiler + * Add support to `sudo` if necessary + * Removed/updated obsolete Doxygen configuration options + * Disabled Doxygen by default + * ADT/Ref.h: remove header + * Updated test MemoryLimit.c to use FileCheck, and formatted the file + * Document that GetTotalMallocUsage returns the usage in bytes +- add shlib-policy-name-error filter to rpmlint (for 15.4) + +------------------------------------------------------------------- +Wed Mar 16 09:05:12 UTC 2022 - jslaby@suse.cz + +- Update to version 2.2+20220311: + * FD_Fail: use /dev/zero instead of /etc/mtab + * Core/Executor: Fix unaligned write of fp80 arguments + * Core/ExecutionState: Fix uninitialized reads in unit tests + * CI: add `-fno-sanitize-recover=undefined` to UBSAN flags + * tests: make UBSAN print stack traces + * CI: drop `-fsanitize=integer` from UBSAN flags + * CI: Update GTest to 1.11.0 + * CI: Update Z3 to 4.8.14 + * build: fix missing target for grep + * fix CMake: gtest from llvm includes gtest_main + * and many more +- delete (they are all upstream) + * 0001-Support-FileHandling.cpp-rewrite-to-C-14.patch + * 0002-llvm13-llvm-fs-F_None-has-been-removed.patch + * 0003-llvm13-llvm-cl-GeneralCategory-is-no-longer-a-global.patch + * 0004-llvm13-CreateLoad-API-with-implicit-types-has-been-d.patch + * 0005-llvm13-CreateGEP-no-longer-accepts-nullptr.patch + * 0006-llvm13-llvm-APInt-toString-has-been-moved-to-StringE.patch + * 0007-llvm13-Add-LLVM-13-to-lit.cfg.patch + * 0008-llvm13-Add-LLVM-13-to-Travis-CI-and-GitHub-Actions.patch + +------------------------------------------------------------------- +Tue Oct 19 07:47:49 UTC 2021 - jslaby@suse.cz + +- Update to version 2.2+20211017: + * test/Runtime/POSIX/Futimesat: futimesat(2) requires _GNU_SOURCE on glibc platforms + * test/Runtime/POSIX/Futimesat: Compile with -std=c99 + * test/Feature/FunctionAlias.c: Add missing CHECK-UNKNOWN prefix +- add llvm 13 support + * 0001-Support-FileHandling.cpp-rewrite-to-C-14.patch + * 0002-llvm13-llvm-fs-F_None-has-been-removed.patch + * 0003-llvm13-llvm-cl-GeneralCategory-is-no-longer-a-global.patch + * 0004-llvm13-CreateLoad-API-with-implicit-types-has-been-d.patch + * 0005-llvm13-CreateGEP-no-longer-accepts-nullptr.patch + * 0006-llvm13-llvm-APInt-toString-has-been-moved-to-StringE.patch + * 0007-llvm13-Add-LLVM-13-to-lit.cfg.patch + * 0008-llvm13-Add-LLVM-13-to-Travis-CI-and-GitHub-Actions.patch +- switch to llvm 13 + +------------------------------------------------------------------- +Mon Oct 04 10:57:30 UTC 2021 - jslaby@suse.cz + +- Update to version 2.2+20210915: + * LLVM 12 support + * Test failure for WSL 1 +- delete (they are upstream) + * 0001-llvm12-VectorType-getNumElements-has-been-deprecated.patch + * 0002-llvm12-Add-LLVM-12-to-lit.cfg.patch + * 0005-llvm12-Implement-llvm.-s-u-max-min-intrinsics.patch + * 0006-llvm11-Handle-llvm.roundeven-instrinsic.patch + * 0007-llvm12-Implement-llvm.abs-intrinsic.patch + +------------------------------------------------------------------- +Fri May 28 05:52:48 UTC 2021 - Jiri Slaby + +- Update to version 2.2+20210510: + * allocate memory objects for functions + * differentiate between partial and completed paths in summary and fix paths + stats when not dumping states + * posix runtime: add malloc checks + * Fix erroneous klee-stats legend for --print-all + * Replaced the time-based delay + * Refactored maxStaticPctChecks into a sequence of conditions. + * Added a warning when forking is skipped due to MaxStatic*Pct limits being + reached + * Added -max-static-pct-check-delay to replace the hardcoded delay after + which the MaxStatic*Pct checks are performed. + * klee-replay: Fix -Wformat-truncation warning +- Switch to LLVM 12. (patches from pr#1389 + 1) + * 0001-llvm12-VectorType-getNumElements-has-been-deprecated.patch + * 0002-llvm12-Add-LLVM-12-to-lit.cfg.patch + * 0005-llvm12-Implement-llvm.-s-u-max-min-intrinsics.patch + * 0006-llvm11-Handle-llvm.roundeven-instrinsic.patch + * 0007-llvm12-Implement-llvm.abs-intrinsic.patch + * 0001-test-disable-until-it-is-fixed.patch + +------------------------------------------------------------------- +Tue Feb 23 07:33:34 UTC 2021 - jslaby@suse.cz + +- Update to version 2.2+20210222: + * runtime/POSIX: fix failures with glibc-2.33 +- remove 0001-runtime-POSIX-fix-failures-with-glibc-2.33.patch + +------------------------------------------------------------------- +Fri Feb 19 07:15:02 UTC 2021 - jslaby@suse.cz + +- Update to version 2.2+20210216: + * Executor: remove obsolete special case for __cxa_{re,}throw + * add klee_messages for C++ exception handling support + * add ifdefs for C++ exception handling + * renaming 'libcxx' -> 'libc++' + * posix runtime: getcwd: check malloc and set errno + * posix runtime: remove dead branch + * klee-libc: simplify mempcpy + * fix cflags for runtime build types +- add 0001-runtime-POSIX-fix-failures-with-glibc-2.33.patch + +------------------------------------------------------------------- +Sun Dec 13 14:44:36 UTC 2020 - Aaron Puchert + +- Update version to 2.2: the biggest changes are C++ exception + support and additional runtime libraries. + * Only build 32bit runtime libraries if supported by platform + * Compatibility with LLVM 11. + * Declare mempcpy on macOS, to silence compiler warnings + * Handle LLVM version selection more robust + * Use non-interactive input + * p-klee.inc: libc++abi only needed for c++ exception support + * slightly improve C++-related CMake strings + * fix CMake: libcxxabi is only required with KLEE_EH_CXX + * tests: add test for klee-stats --table-format=csv/readable-csv + * klee-stats: add (readable) csv format (--table-format=readable-csv/csv) + * Do not redefine fgetc_unlocked and fputc_unlocked unconditionally. + * Added fortified library (for -D_FORTIFY_SOURCE), to be linked when uc… + * Test checking that __memchk_chk is handled correctly with the freesta… + * Rename FreeStanding to Freestanding where appropriate + * [build] Add multilib package to build 32bit on ubuntu + * Link to the different runtime libraries depending on the application … + * [cmake] Add support to generate arbitrary runtime library configurations + * [cmake] Always create KLEE runtime directory even if POSIX is not built + * [cmake] Remove clean_all target as not needed by any additional target + * [cmake] Use clean command to remove generated doxygen files + * [cmake] Remove several leftovers from old autoconf build system + * [cmake] Switch to "newer" cmake version 3.5.0 + * fix: bcmp with n==0 + * Call functions in __cxa_atexit in reverse order + * Optimize StaticDestructor test to be less fragile to compiler optimiz… + * fix Executor: remove UB from bindInstructionConstants + * DFS/BFS/RandomSearcher: replace loop with std::find + * MergingSearcher: remove random-path incompatibility + * searchers: clean up, add documentation + * address MartinNowack's remaining feedback + * README-CMAKE.md: add C++ related variables + * Exception handling only for LLVM >= 8.0.0 + * use isa<> and explicit nullptr-check for compilation with older LLVM … + * Implemented support for C++ Exceptions + * implement fneg instruction + * fix: fabs() working on the wrong argument + * Explicitly track global variables in getDirectCallTarget + * Added support for klee_open_merge and klee_close_merge in replay, tog… + * klee-stats: fix behaviour for broken/empty DBs + * Add check if KLEE is installed + * [CMake][Z3] Check if function `Z3_get_error_msg` needs `context` usin… + * Remove shebang from include + * Fix LLVM 4.0 build patch + * Replace llvm::CallSite with llvm::CallBase on LLVM 8+ +- Go with regular release for now. +- Switch to LLVM 11. + +------------------------------------------------------------------- +Wed Sep 23 07:11:05 UTC 2020 - jslaby@suse.com + +- Update to version 2.1+20200921: + * Added a PR template, with a checklist documenting the most frequent issues we have encountered + * [gen-bout] Support multiple symbolic files + * Add klee-zesti a ZESTI like wrapper script + * Fix codecov upload + * Remove secure vars + * Guard process-tree compression with a command-line switch + * More robust handling of unknown intrinsics + * Definition of __cxa_thread_atexit_impl for the KLEE libc. + * klee-stats: check for a run.stats file in the klee-out directory, to prevent outputting wrong data. + * DiscretePDF: use IDs instead of pointers (see PR #739) + * New intrinsic: klee_is_replay +- disable 32 bit archs as klee doesn't (and won't) build on them + +------------------------------------------------------------------- +Thu Aug 06 09:35:38 UTC 2020 - jslaby@suse.com + +- Update to version 2.1+20200730: + * introduce --rng-initial-seed= + * remove holes in Instruction-/FunctionInfoTable, add documentation + * Clean-up and add documentation + * Remove state contructor with constraints + * Use constraint sets and separate metadata for timing solver invocation + * Separate constraint set and constraint manager + * Move constraint implementation from header to cpp files + * Enable subsets for RandomPathSearcher + * [PTree] Replace left/right with PointerIntPair + * Implement fshr/fshl intrinsics + * Switch to a more recent version of SQLite in the CI + * Enforce fork/branch limits in branch() and fix double termination + * fix Executor: initializeGlobalAliases + * ExecutorUtil: assert that GlobalValue is already known + * add simple unknown bitcast alias test from the original issue + * and more +- switch to obs_scm + +------------------------------------------------------------------- +Tue Jun 09 07:08:47 UTC 2020 - jslaby@suse.com + +- Update to version 2.1+20200606: + * [Module] Add testcase for inline asm lifting + * [Module] Disable lifting for inline asm resembling memory fences with return values + * Add test case from #1257 to reproduce behaviour + * [Solver:STP] Fix handling of array names + * docker: install KLEE headers in system include path + * Moved header files that were placed directly in include/klee/ into appropriate existing directories and a new directory Statistics; a few missing renames. + * Removed include/klee/util and moved header files to appropriate places + * Created include/klee/Core directory and moved appropriate files direc\ tly in lib/Core + * Move header files from lib/Expr to include/klee/Expr to eliminate includes using "../" + * Removed the Internal directory from include/klee + +------------------------------------------------------------------- +Sat Apr 25 22:10:44 UTC 2020 - aaronpuchert@alice-dsl.net + +- Update to version 2.1+20200420: + * Consistently define variable using notation VAR=value; fixed comment placement + * Named jobs in Travis CI for better visualization of results + * [posix-runtime] Improve model to handle full-path symbolic files + * [posix-runtime] Add test for full path consistency for symbolic files + * readStringAtAddress: support pointer into objects + * test: add a new test for readStringAtAddress + * readStringAtAddress: use stringstream to obtain the string + * stats: rename QueriesConstructs to QueryConstructs + * Statistic: slightly modernise class definition + * stats: remove queryConstructTime (unused) + * Add unit test for Z3Solver::getConstraintLog + * Run "pkg update -f" before installing dependencies on FreeBSD + * Don't search for CryptoMiniSAT when configuring STP + * Fixed some messages, particularly Klee -> KLEE + * Ensure that temp_builder is used when adding constant array value assertion constraints + * StatsTracker: remove NumObjects, fix assignment of and always write ArrayHashTime + * [posix-runtime] Simple GET/SET_LK model + * Additional test for dealing with vector instructions + * Added another `ScalarizerLegacyPass` run to remove vectorized code introduced during the optimization step + * Fixed compiler warning when printing variable of type off_t + * stat64 is deprecated on macOS; use stat instead + * Use -snap VMs on Cirrus for FreeBSD + * Updating KLEE's version post-release + * Release notes for 2.1 + * Set version to 2.1 + * fix lit.cfg: numerical comparison of LLVM version numbers + * travis: add LLVM 10.0 + * test/lit.cfg: add LLVM 10.0 + * stats: enforce table creation + * [klee-stats] Grafana: Limit number of entries to query for column names + * [klee-stats] Use the last row inserted instead of the row with highest Instructions + * [klee-stats] Refactor preparing and printing the table + * [klee-stats] Check for existence of stats file for Grafana as well + * [klee-stats] Do not crash if tabulate is not installed but requested + * [klee-stats] Refactor writing table into own function + * [klee-stats] Refactor CSV printout in own function + * [klee-stats] Check if stats file exist before trying to open it + * Add leading zeros to genbout + * fix p-llvm.inc: invocation for monorepo directory layout + * find_llvm.cmake: enable parsing for git version + * Use FreeBSD 11.3-STABLE instead of EoLed 11.2. + * Workaround `pkg` breakage on FreeBSD CI. + * Use `ref<>` for MemoryObject handling + * Use `ref<>` for UpdateNode + * Clean-up header files + * Add move assignment operator and move construct for `ref` class. + * Add `ReferenceCounter` struct utilized by ref<> + * Fix ptr reference invalidation if last reference gets freed before new reference assigned. + * Use call-by-reference for hash-function invocation + * Replace old TR1 implementations of unordered_map/set with std::* versions + * Use a newer Ubuntu 18.04 from the year 2020 to build KLEE Dockerimage + * Use a newer Ubuntu 18.04 from the year 2020 to build KLEE + * Update Docker image template for KLEE. + * Use system's boost when building metasmt and user newer boolector version + * Do not wait if SANITIZER_BUILD is empty + * Add llvm as build dependency of clang in case no system packages are available + * Add patch support for libcxx + * Use git repository to build LLVM + * Update ubuntu build dependencies for KLEE + * update +- Switch to LLVM 10. +- Disable assertions. +- Take "FileCheck" and "not" from official git repository. + +------------------------------------------------------------------- +Fri Jan 24 07:34:10 UTC 2020 - jslaby@suse.com + +- Update to version 2.0+20200119: + * Remove statistics limit from istats. + * Fix handling of debug information for functions + * Update objdump script to support python3 + * Fixed documentation for command line argument link-llvm-lib + * Assume assembly.ll is local to the run.istats file + * Remove unnecessary std::move's that prevent copy elision + * [optimize-array] Fix value transformation + * [optimize-array] Fix hole index in buildMixedSelectExpr + * [optimize-array] Fix hash collisions + * [optimize-array] Hash collision test + * [optimize-array] Fix update list read order + * [Searchers] Remove weight from es, add nurs_depth + * Move merging related code from Executor into MergingSearcher + * Implement @llvm.is.constant() intrinsic handling and add a test for it. + * [expr-visitor] Remove unnecessary allocation + * Handle llvm.objectsize explicitly + * Added test for 3-argument main. + * Allow main with 3 arguments + * Most libc++ tests require uclibc; add missing REQUIRES statements or remove dependency. + * Core: Executor, remove unused variable + * Do not modify strings if they are read-only. + * Mark all constant global memory objects as constant + * [test] Fix missing includes + * runtime: fix for glibc 2.30 + * Remove the duplicated check for DebugInfoIntrinsic +- Remove 0001-runtime-workaround-for-glibc-2.30.patch (upstreamed) + +------------------------------------------------------------------- +Mon Nov 04 06:50:43 UTC 2019 - jslaby@suse.com + +- switch to llvm 9 +- Update to version 2.0+20191031: + * Executor: fix missing default case in switch instruction + * enable testing for LLVM 9.0 + * LLVM 9.0: fourth parameter for @llvm.objectsize() + * klee-libc: add bcmp + * support compilation against LLVM 9.0 + * [klee-replay] Fix relative executable paths + * ExecutorTimers: refactor and move to support lib + * ExecutorTimers: remove signalling, fix endless looping fork + * Executor.h: remove defined functions without implementation + * test/Expr/Evaluate2.kquery: add link to issue + * fix: make llvm 7.1 known + * test/Feature/SolverTimeout.c: re-enable for Z3 + * test/lit.cfg: test if current version is known + * test/lit.cfg: use lit_config instead of lit + * Do not use klee_range() in regression/2014-09-13-debug-info.c test, as it is incompatible with klee_prefer_cex. Fixes https://github.com/klee/klee/issues/1161 + +------------------------------------------------------------------- +Fri Oct 04 10:39:23 UTC 2019 - jslaby@suse.com + +- Update to version 2.0+20190920: + * Add saturated arithmetic intrinsics + * fixed bug in IntrinsicCleaner trap cleaner + * StatsTracker: switch from TRUNCATE to WAL journal mode + * Read Klee's start time correctly in klee-stats + * CMake: show values of optional LLVM variables + * Provide klee runtime build type as parameter + * PTree: fix dump() method + * ExecutionState: remove fnAliases + * implement FunctionAliasPass + * remove klee_alias_function() + * Implement handling of the llvm.fabs intrinsic + * and more fixes +- drop unused disable-failing-test.patch +- add 0001-runtime-workaround-for-glibc-2.30.patch + +------------------------------------------------------------------- +Mon Jul 12 23:35:27 UTC 2019 - Aaron Puchert + +- Use -flto=thin instead of -flto= for Clang. + +------------------------------------------------------------------- +Mon Jul 1 23:16:30 UTC 2019 - Aaron Puchert + +- Switch to LLVM 8. + +------------------------------------------------------------------- +Mon May 27 09:39:22 UTC 2019 - jslaby@suse.com + +- Update to version 2.0+20190507: + * Propagate correct version of metasmt to build script + * Add missing dependency for tabulate package + * Remove CC as requirement; automatically set by sanitizer_compiler + * klee-stats: add - to to-csv/grafana options + * Add klee-stats test, fix microseconds bug + * Add MSan support for sqlite + * Clean klee-stats, StatsTracker and cmake + * Change the .stats format into sqlite3 + * Add FreeBSD OS triple in RaiseAsm + * Teach ConcreteTest.py to use `gmake` instead of `make` on FreeBSD + * and more + +------------------------------------------------------------------- +Mon Feb 25 10:15:41 UTC 2019 - Jiri Slaby + +- Update to version 1.4.0+20190115: + * make AssignmentLessThan::operator() const-invocable + * fix a bug in a function call + * ktest-tool: move from optparse to argparse, add ouput/example sections to help + * Travis OSX: install Python 3.x + * regression/2014-09-13-debug-info.c: use 'int: ' instead of 'data:' + * Various fixes for ktest-tool + * Added default values to option comments + * Renamed --environ to --env-file + * Renamed --stop-after-n-tests to --max-tests + * Added a replaying option category + * Added checks option category, moved --optimize to starting category, renamed original --run-in option to --running-dir + * Added linking option category + * Added starting option category + * Added test case option category + * Added debugging category + * Renamed --stop-after-n-instructions to --max-instructions, as suggested by @251 + * Added some descriptions suggested by @MartinNowack and placed --max-static-... options under the termination category of options + * Added option categories for external call policy and termination criteria + * Created two more option categories: test generation and seeding. + +------------------------------------------------------------------- +Sun Dec 16 09:33:44 UTC 2018 - Jiri Slaby + +- Update to version 1.4.0+20181214: + * Enable C++14 support + * Implemented memalign with alignment + * Use LLVM 4 for Mac Build + * Fix bug which resulted in an incorrect warning to be printed. + * fix: actually set -O0 in test/concrete/CMakeLists.txt + * Fixed crash on zero size arrays + * Check for stack overflow in a tested program + * Added test for the case where external calls are encountered but disallowed + * Replaced --no-externals and --allow-external-sym-calls with --external-calls, updated tests accordingly, and improved documentation on external calls + * The test DeterministicSwitch.c does not need to allow external symbolic calls + * Introduced a constraint solving option category to which all the options in CmdLineOptions.cpp are currently added. + * Base time API upon std::chrono + * add %OOopt to recently added tests and Concrete + +------------------------------------------------------------------- +Mon Oct 29 16:28:27 UTC 2018 - Jiri Slaby + +- switch to LLVM 7 +- add disable-failing-test.patch + +------------------------------------------------------------------- +Sat Oct 27 07:24:23 UTC 2018 - opensuse-packaging@opensuse.org + +- Update to version 1.4.0+20181026: + * travis: enable LLVM 7 testing + * llvm7: handle new header files + * llvm7: adapt to new openFileForWrite + * llvm7: WriteBitcodeToFile takes Module & + * Added gen-bout tool to generate ktest file (file.bout) using specified concrete arguments and files. + * travis: enable LLVM 6 testing + * llvm6: handle headers renaming + * llvm6: SetVersionPrinter now passes down a stream + * travis: enable LLVM 5 testing + * llvm5: APInt->getSignBit -> getSignMask + * llvm5: CallSite.paramHasAttr is indexed from 0 + * llvm5: test, add -disable-O0-optnone to -O0 + * llvm5: test, change objectsize + * llvm5: Intrinsic::objectsize has three arguments + * llvm5: use MutableArrayRef for APFloat::convertToInteger + * llvm5: handle new file_magic's location + * llvm5: SwitchInst case functions now return pointers + * llvm5: handle getOrInsertFunction terminator + * llvm5: integerPartWidth is from llvm::APFloatBase + * llvm5: avoid ++ on function->arg_begin() + * Add testcase for shift check + * ShiftChecker: Instrument shift instructions only once + * ShiftChecker: Avoid unneeded checks + * ShiftCheck: Use llvm::Builder instead of Inst::Create* + * Add test case for div checker + * DivCheck do not instrument multiple times + * DivCheck Skip unneeded checks + * Use llvm::Builder for DivCheck instrumentation + * Introduce KLEEIRMetaData to manipulate LLVM-IR metadata + * Added lowering pass + * refactor klee_open_output_file to return std::unique_ptr + * use klee_open_output_file for uncompressed logs + * Updated an include to reflect a recent filename change + * Move unrelated function from ReadExpr class + * Avoid unsafe static downcasts + * Modernize code + * Move optimization specific headers away from the project include directory + * Clean-up headers + * Use std::unordered collections as we use C++11 + * Remove unneeded externs + * Remove condition check before function invocation + * Move ConstantExpr check inside optimizeExpr function + * optimizeExpr: return the result as return value instead as function argument + * Make valueOnly parameter of optimizeExpr explicit + * Fixed compilation of array optimization patch with LLVM >= 4.0 + * Added missing headers and clang-format the files + * Added support for KLEE value-based array optimization + * Added support for KLEE index-based array optimization + * tests: disable CompressedExprLogging on zlib-less systems + * Small changes to comments + * Added missing header to SolverCmdLine.h and clang-format it + * Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant to have only solver options. + * fix handling of failing external calls + * cmake/lit: add asan/non-asan, ubsan/non-ubsan flags + * cleanup headers, whitespaces, and types + * add support for klee-replay on OSX + * Workaround for flaky coverage + * kleeModule: always link irreader (required since llvm 3.3) + * remove obsolete dependency of kleeModule on kleeCore + * config.h.cmin: remove obsolete cmakedefine + * Marking resolve methods as const + * Refactored AddressSpace::resolve() by creating a new function AddressSpace::checkPointerInObject() that is called in both the forward and the backward searches. This makes the code more modular and removes a large part of duplicated code and should also address the non-deterministic coverage in the resolve() function which affects Codecov reports. + * Fix a crash when the last running state is terminated during merging + * Changed code to create up to 100 properly-numbered symbolic arguments, and add a corresponding check. + * Add checks for correct usage of the POSIX model, together with an associated test. + * Revert lit to 0.6.0 version, as 0.7.0 misbehaves +- removed (in upstream): + * 0001-llvm5-avoid-on-function-arg_begin.patch + * 0002-llvm5-integerPartWidth-is-from-llvm-APFloatBase.patch + * 0003-llvm5-handle-getOrInsertFunction-terminator.patch + * 0004-llvm5-SwitchInst-case-functions-now-return-pointers.patch + * 0005-llvm5-handle-new-file_magic-s-location.patch + * 0006-llvm5-use-MutableArrayRef-for-APFloat-convertToInteg.patch + * 0007-llvm5-Intrinsic-objectsize-has-three-arguments.patch + * 0008-llvm5-test-change-objectsize.patch + * 0009-llvm5-test-add-disable-O0-optnone-to-O0.patch + * 0010-llvm5-CallSite.paramHasAttr-is-indexed-from-0.patch + * 0011-llvm6-SetVersionPrinter-now-passes-down-a-stream.patch + * 0012-llvm6-handle-headers-renaming.patch + +------------------------------------------------------------------- +Fri Sep 21 11:24:38 UTC 2018 - jslaby@suse.com + +- Update to version 1.4.0+20180920: + * Removed unused file + * Removed unused --sym-files 0 0 argument from FD_Fail test and rewrote the test to use FileCheck instead of grep + * Updated IoCtl test to use --sym-stdin instead of --sym-files 0 x to make stdin symbolic and removed unused arguments to main. + * Updated DirSeek test to use --sym-stdin instead of --sym-files 0 x to make stdin symbolic. + * Silence an uninitialized variable compiler warning (and a tiny formatting change) + * travis: enable LLVM 4 testing + * llvm4: gep_type_iterator has no operator* + * llvm4: PointerType is not SequentialType + * llvm4: use chrono helpers from LLVM + * llvm4: errorOr and similar + * llvm4: APFloat members are functions + * llvm4: handle different header names + * travis CI: add LLVM 3.9 build tests + * llvm39: switch KLEE_RUNTIME_BUILD_TYPE to Debug+Asserts + * cmake: find_llvm, fix libraries with llvm-config 3.9 + * llvm: make KLEE compile against LLVM 3.9 + * Add testcase to run POSIX environment and main without arguments + * Add POSIX runtime as dependency for the test case + * Unify the error message if that function has not been found. + * Fix generation of global constructors and destructors + * POSIX: Add invocation of klee_init_env into wrapper before calling main + * Fix missing includes and declarations + * Use FileCheck and LINE instead of grep if possible + * llvm36.patch: fix build for newer glibc/gcc versions + * runtime: fix memory error in canonicalize_file_name + * Build on trusty without sudo - uses faster Docker infrastructure from TravisCI + * Avoid Vararg non-deterministic allocation +- removed (in upstream): + * 0001-llvm-make-KLEE-compile-against-LLVM-3.9.patch + * 0002-cmake-find_llvm-fix-libraries-with-llvm-config-3.9.patch + * 0003-llvm39-switch-KLEE_RUNTIME_BUILD_TYPE-to-Debug-Asser.patch + * 0004-llvm40-handle-different-header-names.patch + * 0005-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + * 0006-llvm40-errorOr-and-similar.patch + * 0007-llvm-use-chrono-helpers-from-LLVM-4.0.patch + * 0008-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + * 0009-llvm40-gep_type_iterator-has-no-operator.patch +- removed (not needed): + * 0017-llvm50-Intrinsic-objectsize-has-three-arguments.patch +- renamed: + * 0010-llvm50-avoid-on-function-arg_begin.patch + -> 0001-llvm5-avoid-on-function-arg_begin.patch + * 0011-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + -> 0002-llvm5-integerPartWidth-is-from-llvm-APFloatBase.patch + * 0012-llvm50-handle-getOrInsertFunction-terminator.patch + -> 0003-llvm5-handle-getOrInsertFunction-terminator.patch + * 0013-llvm50-SwitchInst-case-functions-now-return-pointers.patch + -> 0004-llvm5-SwitchInst-case-functions-now-return-pointers.patch + * 0014-llvm50-handle-new-file_magic-s-location.patch + -> 0005-llvm5-handle-new-file_magic-s-location.patch + * 0015-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + -> 0006-llvm5-use-MutableArrayRef-for-APFloat-convertToInteg.patch + * 0016-llvm50-AllocaInst-takes-address-space.patch + -> 0007-llvm5-Intrinsic-objectsize-has-three-arguments.patch + * 0018-llvm50-test-change-objectsize.patch + -> 0008-llvm5-test-change-objectsize.patch + * 0019-llvm50-test-add-disable-O0-optnone-to-O0.patch + -> 0009-llvm5-test-add-disable-O0-optnone-to-O0.patch + * 0020-llvm50-CallSite.paramHasAttr-is-indexed-from-0.patch + -> 0010-llvm5-CallSite.paramHasAttr-is-indexed-from-0.patch + * 0021-llvm6-SetVersionPrinter-now-passes-down-a-stream.patch + -> 0011-llvm6-SetVersionPrinter-now-passes-down-a-stream.patch + * 0022-llvm6-handle-headers-renaming.patch + -> 0012-llvm6-handle-headers-renaming.patch + +------------------------------------------------------------------- +Sun Sep 02 08:39:37 UTC 2018 - opensuse-packaging@opensuse.org + +- Update to version 1.4.0+20180829: + * klee-stats: add TResolve(%) to --print-all + * llvm.sh: fix patch source paths + * Disabled unit testing in default build + * Fixed runtest library to handle the case of a NULL "name" argument in klee_make_symbolic. Changed a test case to check this feature. + * Replace remaining *Inst::Create() calls with llvm::Builder + * [clang-format]Allow longer codelines in test/ + * test: remove geq-llvm-3.4 + * remove last comma from -debug-print-escaping-functions + * test/Feature/EscapingFunctionsAlias.c: clarify alias(ee) casting + * add declarations to escapingFunctions + * ModuleUtil: improve and test valueIsOnlyCalled + * fix: LLVM 3.5, begin_user() instead of begin_use() + * ExternalDispatcher: setErrorStr for EngineBuilder + * travis CI: add LLVM 3.8 build tests + * llvm38: test, change some tests + * llvm38: no more implicit iterators + * llvm38: archive child iterator changes + * llvm38: adapt to new Linker::linkModules + * llvm38: SmallString is always up-to-date + * llvm38: handle optimization passes changes + * llvm38: no rounding in APFloat + * Fix uploading of coverage information from inside of docker + * Add missing curl + * Fix slow Mac Travis build: wildcard is not expanded with quotes + * Added "override" in Executor.h to silence compiler warnings (and ran clang-format on patch) + * Removed support for klee_make_symbolic with 2 arguments. This has been deprecated for many years now and causes problems during replay. Changed and simplified affected test case. + * test: remove undefined behaviour + * Enabled tcmalloc by default + * Link dynamic libraries with specific paths instead of resolving them during runtime + * Fix incorrect invocation of klee + * Fix uninitialized memory: enums have to be initialized + * Add missing out-of-tree include files directory for TCMalloc + * Fix compiler warnings if assertions are disabled + * Support sanitizer suppression files with lit-based testing + * Extensive updates to the build script for dependencies and docker + * runtime: remove obsolete code for building modules instead of archives + * Reorder linking and optimizations + * Reorganise runtime libraries provided by KLEE + * Removed obsolete script + * test/lit.cfg: remove obsolete hack from (LLVM < 3.0 is no longer supported) + * CMake: use cmake_{push,pop}_check_state + * CMake: check for ctype and mallinfo functions with CXX instead of C compiler + * fix out of range access in KleeHandler::getKTestFilesInDir + * Explicitly initialize value to squelch a potentially uninitialized value warning + * Fix the final -Wimplicit-fallthrough warning + * Make ConstantExpr hashing function faster and modify affected test +- added patches: + * 0003-llvm39-switch-KLEE_RUNTIME_BUILD_TYPE-to-Debug-Asser.patch + * 0005-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + * 0020-llvm50-CallSite.paramHasAttr-is-indexed-from-0.patch +- removed patches (in upstream now): + * 0001-test-remove-undefined-behaviour.patch + * 0002-llvm38-no-rounding-in-APFloat.patch + * 0003-llvm38-handle-optimization-passes-changes.patch + * 0004-llvm38-SmallString-is-always-up-to-date.patch + * 0005-llvm38-materializeAllPermanently-was-renamed.patch + * 0006-llvm38-adapt-to-new-Linker-linkModules.patch + * 0007-llvm38-archive-child-iterator-changes.patch + * 0008-llvm38-no-more-implicit-iterators.patch + * 0009-llvm38-test-change-some-tests.patch +- renamed patches: + * 0010-llvm-make-KLEE-compile-against-LLVM-3.9.patch + -> 0001-llvm-make-KLEE-compile-against-LLVM-3.9.patch + * 0011-cmake-find_llvm-fix-libraries-with-llvm-config-3.9.patch + -> 0002-cmake-find_llvm-fix-libraries-with-llvm-config-3.9.patch + * 0012-llvm40-handle-different-header-names.patch + -> 0003-llvm39-switch-KLEE_RUNTIME_BUILD_TYPE-to-Debug-Asser.patch + * 0013-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + -> 0004-llvm40-handle-different-header-names.patch + * 0014-llvm40-errorOr-and-similar.patch + -> 0006-llvm40-errorOr-and-similar.patch + * 0015-llvm-use-chrono-helpers-from-LLVM-4.0.patch + -> 0007-llvm-use-chrono-helpers-from-LLVM-4.0.patch + * 0016-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + -> 0008-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + * 0017-llvm40-gep_type_iterator-has-no-operator.patch + -> 0009-llvm40-gep_type_iterator-has-no-operator.patch + * 0018-llvm50-avoid-on-function-arg_begin.patch + -> 0010-llvm50-avoid-on-function-arg_begin.patch + * 0019-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + -> 0011-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + * 0020-llvm50-handle-getOrInsertFunction-terminator.patch + -> 0012-llvm50-handle-getOrInsertFunction-terminator.patch + * 0021-llvm50-SwitchInst-case-functions-now-return-pointers.patch + -> 0013-llvm50-SwitchInst-case-functions-now-return-pointers.patch + * 0022-llvm50-handle-new-file_magic-s-location.patch + -> 0014-llvm50-handle-new-file_magic-s-location.patch + * 0023-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + -> 0015-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + * 0024-llvm50-AllocaInst-takes-address-space.patch + -> 0016-llvm50-AllocaInst-takes-address-space.patch + * 0025-llvm50-Intrinsic-objectsize-has-three-arguments.patch + -> 0017-llvm50-Intrinsic-objectsize-has-three-arguments.patch + * 0026-llvm50-test-change-objectsize.patch + -> 0018-llvm50-test-change-objectsize.patch + * 0027-llvm50-test-add-disable-O0-optnone-to-O0.patch + -> 0019-llvm50-test-add-disable-O0-optnone-to-O0.patch + * 0028-llvm60-SetVersionPrinter-now-passes-down-a-stream.patch + -> 0021-llvm6-SetVersionPrinter-now-passes-down-a-stream.patch + * 0029-llvm60-handle-headers-renaming.patch + -> 0022-llvm6-handle-headers-renaming.patch + +------------------------------------------------------------------- +Sat Jun 16 09:09:56 UTC 2018 - opensuse-packaging@opensuse.org + +- Update to version 1.4.0+20180614: + * Add unittest for DiscretePDF + * klee_int: allow NULL as name + * cmake: find_llvm, handle libLLVM-version.so properly + * Fixed memory leak from Executor::inCloseMerge, fixes #883 +- Require python3-lit as the lit packaging was refactored +- switch to llvm 6 +- removed patches: + * 0001-llvm-make-KLEE-compile-against-LLVM-3.8.patch + (it was split into multiple commits below) + * klee-skip-some-tests.patch + (tests should be working perfectly now) +- added patches: + * 0001-test-remove-undefined-behaviour.patch + * 0002-llvm38-no-rounding-in-APFloat.patch + * 0003-llvm38-handle-optimization-passes-changes.patch + * 0004-llvm38-SmallString-is-always-up-to-date.patch + * 0005-llvm38-materializeAllPermanently-was-renamed.patch + * 0006-llvm38-adapt-to-new-Linker-linkModules.patch + * 0007-llvm38-archive-child-iterator-changes.patch + * 0008-llvm38-no-more-implicit-iterators.patch + * 0011-cmake-find_llvm-fix-libraries-with-llvm-config-3.9.patch + * 0027-llvm50-test-add-disable-O0-optnone-to-O0.patch +- renamed patches: + * 0002-llvm38-test-change-some-tests.patch + -> 0009-llvm38-test-change-some-tests.patch + * 0003-llvm-make-KLEE-compile-against-LLVM-3.9.patch + -> 0010-llvm-make-KLEE-compile-against-LLVM-3.9.patch + * 0004-llvm40-handle-different-header-names.patch + -> 0012-llvm40-handle-different-header-names.patch + * 0005-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + -> 0013-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + * 0006-llvm40-errorOr-and-similar.patch + -> 0014-llvm40-errorOr-and-similar.patch + * 0007-llvm-use-chrono-helpers-from-LLVM-4.0.patch + -> 0015-llvm-use-chrono-helpers-from-LLVM-4.0.patch + * 0008-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + -> 0016-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + * 0009-llvm40-gep_type_iterator-has-no-operator.patch + -> 0017-llvm40-gep_type_iterator-has-no-operator.patch + * 0010-llvm50-avoid-on-function-arg_begin.patch + -> 0018-llvm50-avoid-on-function-arg_begin.patch + * 0011-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + -> 0019-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + * 0012-llvm50-handle-getOrInsertFunction-terminator.patch + -> 0020-llvm50-handle-getOrInsertFunction-terminator.patch + * 0013-llvm50-SwitchInst-case-functions-now-return-pointers.patch + -> 0021-llvm50-SwitchInst-case-functions-now-return-pointers.patch + * 0014-llvm50-handle-new-file_magic-s-location.patch + -> 0022-llvm50-handle-new-file_magic-s-location.patch + * 0015-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + -> 0023-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + * 0016-llvm50-AllocaInst-takes-address-space.patch + -> 0024-llvm50-AllocaInst-takes-address-space.patch + * 0017-llvm50-Intrinsic-objectsize-has-three-arguments.patch + -> 0025-llvm50-Intrinsic-objectsize-has-three-arguments.patch + * 0018-llvm50-test-change-objectsize.patch + -> 0026-llvm50-test-change-objectsize.patch + * 0019-llvm60-SetVersionPrinter-now-passes-down-a-stream.patch + -> 0028-llvm60-SetVersionPrinter-now-passes-down-a-stream.patch + * 0020-llvm60-handle-headers-renaming.patch + -> 0029-llvm60-handle-headers-renaming.patch + +------------------------------------------------------------------- +Fri May 25 10:57:57 UTC 2018 - opensuse-packaging@opensuse.org + +- Update to version 1.4.0+20180524: + * isLSB should be a boolean, as it is only used in truth contexts + * remove switch fallthrough in floating point comparision + * llvm37: enable travis testing + * llvm37: handle getRegisteredOptions + * test: add versions of some tests for LLVM 3.7 + * llvm: make KLEE compile against LLVM 3.7 + * llvm37: handle GetElementPtrInst::Create's new parameter + * test: add parenthesis around & operands +- removed patches that are in upstream now: + * 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch + * 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch + * 0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch + * 0004-llvm37-handle-getRegisteredOptions.patch +- renamed patches: + * 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch + -> 0001-llvm-make-KLEE-compile-against-LLVM-3.8.patch + * 0007-llvm38-test-change-some-tests.patch + -> 0002-llvm38-test-change-some-tests.patch + * 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch + -> 0003-llvm-make-KLEE-compile-against-LLVM-3.9.patch + * 0008-llvm40-handle-different-header-names.patch + -> 0004-llvm40-handle-different-header-names.patch + * 0009-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + -> 0005-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + * 0010-llvm40-errorOr-and-similar.patch + -> 0006-llvm40-errorOr-and-similar.patch + * 0011-llvm-use-chrono-helpers-from-LLVM-4.0.patch + -> 0007-llvm-use-chrono-helpers-from-LLVM-4.0.patch + * 0012-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + -> 0008-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + * 0013-llvm40-gep_type_iterator-has-no-operator.patch + -> 0009-llvm40-gep_type_iterator-has-no-operator.patch + * 0014-llvm50-avoid-on-function-arg_begin.patch + -> 0010-llvm50-avoid-on-function-arg_begin.patch + * 0015-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + -> 0011-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + * 0016-llvm50-handle-getOrInsertFunction-terminator.patch + -> 0012-llvm50-handle-getOrInsertFunction-terminator.patch + * 0017-llvm50-SwitchInst-case-functions-now-return-pointers.patch + -> 0013-llvm50-SwitchInst-case-functions-now-return-pointers.patch + * 0018-llvm50-handle-new-file_magic-s-location.patch + -> 0014-llvm50-handle-new-file_magic-s-location.patch + * 0019-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + -> 0015-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + * 0020-llvm50-AllocaInst-takes-address-space.patch + -> 0016-llvm50-AllocaInst-takes-address-space.patch +- added patches + * 0017-llvm50-Intrinsic-objectsize-has-three-arguments.patch + * 0018-llvm50-test-change-objectsize.patch + * 0019-llvm60-SetVersionPrinter-now-passes-down-a-stream.patch + * 0020-llvm60-handle-headers-renaming.patch + +------------------------------------------------------------------- +Wed May 23 12:25:13 UTC 2018 - opensuse-packaging@opensuse.org + +- Update to version 1.4.0+20180522: + * clang-format on lib/Module/{IntrinsicCleaner.cpp,Passes.h} + * some housekeeping in Passes.h and IntrinsicCleaner.cpp + * CompressionStream: fix sporadic segfaults (uninitialised avail_in) + * Removed .c_str() from getSourceLocation calls + * Renamed printFileLine to getSourceLocation (as suggested by @delcypher) to reflect the fact that it simply returns a string + * Simplified printFileLine by using std::to_string, and removed unneeded version that takes an argument a stream + * stop using DEBUG macro name + * fix some casts for LLP64 compilers + +------------------------------------------------------------------- +Mon May 21 09:30:16 UTC 2018 - opensuse-packaging@opensuse.org + +- Update to version 1.4.0+20180518: + * tests: use names in klee_make_symbolic + * Delete coverageServer.py + * Abort execution if --only-output-states-covering-new is enabled but its dependency --output-istats is not + * Add support for concretizing symbolic objects passed to external functions + * Improve error messages for ReadStringAtAddress + * Improved code quality + * Implemented incomplete merging + * remove QueryLog.h + * Update clang-format standard for KLEE codebase to C++11 + * Fix test case to check for correct call string + * Improve handling of constant array in Z3 + * Remove the option for truncating lines in assembly.ll + * Remove workaround for bug in older LLVM version (< 3) + * Fix include files + * remove unused file: tools/klee/Debug.cpp + * Fixed test case to exercise modification to utimes() + * Fixed utimes() behavior for symbolic files when the second argument is NULL + * Moved regression test to proper location. Fixes #705 + * Fix handling of errno if external functions are invoked + * Factor out method to update state memory with process state + * Ensured program reliably has 3 paths to be explored, and removed unnecessary options. Make klee_abort() call abort() in replay, and removed trivial test which cannot be easily integrated into the test suite. + * Implement klee_prefer_cex() and klee_abort() in Runtest and added corresponding tests + * add blockaddress and indirectbr instructions + * fix compilation warning + * exitOnError no output buf fix + * Change llvm apt repository to enable llvm 3.7+ + * Fix python2 linking + * doDumpStates: incorrectly increments stats + * [CMake] Add option to set GTest include dir + * fix test/Feature/BFSSearcherAndDFSSearcherInterleaved.c to use explicit enumeration of possible strings instead of CHECK-SAME (does not work as intended with LLVM >= 3.7) + * Store CexCache stats and then update klee-stats to use them + * Add missing endian information to avoid selecction of big endian systems + * Fail for aggegrations with big endian ordering + * Fixed handling of constant vectors with complex data + * Test complex constant data vectors as well + * Make print function of ObjectState public and const + * Add testcase for constant array handling + * Add test case for constant vector init + * Fix correct element order of InsertElement/ExtractElement + * Fix getelementptr for array or vector indices + * Fix generation of expressions from constant sequential data + * Added comment for getPointerWidth + * llvm50: use auto variable instead of SwitchInst::CaseIt + * Enable caching for travis-ci + * Fix coverage generation + * MergeHandler: remove unused closedStateCount + * add wllvm to the python packages to be installed + * [Travis-CI] Added codecov.io support +- Dropped patches (they are in upstream already): + * 0001-MergeHandler-remove-unused-closedStateCount.patch + * 0002-llvm50-use-auto-variable-instead-of-SwitchInst-CaseI.patch + * 0001-Fix-generation-of-expressions-from-constant-sequenti.patch + * 0002-Fix-getelementptr-for-array-or-vector-indices.patch + * 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch + * 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch + * 0005-Track-errno-correctly.patch + * 0006-Declare-klee_get_errno-and-remove-local-declarations.patch + * 0007-Add-support-for-modelling-errno_location.patch + * 0008-Cleanup-test-cases.patch + * 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch + +------------------------------------------------------------------- +Wed Jan 24 07:59:06 UTC 2018 - jslaby@suse.com + +- Add klee-skip-some-tests.patch + +------------------------------------------------------------------- +Mon Jan 15 10:24:53 UTC 2018 - jslaby@suse.com + +- Update to version 1.4.0+20180108: + * [NFC] Remove unused config header template that was only used by the old build system (now removed). + * fix regression test: use `%klee` instead of `klee` + * fix merging tests: use `%klee` instead of `klee` + * Move Homebrew tap from personal repository to the KLEE organization + * Updated TravisCI to use pip2 instead of pip + * Bumped xcode version for TravisCI + * Implemented bounded merging functionality + * Added pause and continue functionality for states in Executor + * Replace confusing message in lit.site.cfg.in about the file being autogenerated + * klee_make_symbolic: add test cases for API + * klee_make_symbolic: warn on deprecated usage +- added patches: + * 0001-MergeHandler-remove-unused-closedStateCount.patch + * 0002-llvm50-use-auto-variable-instead-of-SwitchInst-CaseI.patch + * 0013-llvm40-gep_type_iterator-has-no-operator.patch + * 0014-llvm50-avoid-on-function-arg_begin.patch + * 0015-llvm50-integerPartWidth-is-from-llvm-APFloatBase.patch + * 0016-llvm50-handle-getOrInsertFunction-terminator.patch + * 0017-llvm50-SwitchInst-case-functions-now-return-pointers.patch + * 0018-llvm50-handle-new-file_magic-s-location.patch + * 0019-llvm50-use-MutableArrayRef-for-APFloat-convertToInte.patch + * 0020-llvm50-AllocaInst-takes-address-space.patch +- renamed patches: + * 0013-llvm38-test-change-some-tests.patch -> + 0007-llvm38-test-change-some-tests.patch + * 0007-llvm40-handle-different-header-names.patch -> + 0008-llvm40-handle-different-header-names.patch + * 0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch -> + 0009-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + * 0009-llvm40-errorOr-and-similar.patch -> + 0010-llvm40-errorOr-and-similar.patch + * 0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch -> + 0011-llvm-use-chrono-helpers-from-LLVM-4.0.patch + * 0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch -> + 0012-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + * 0012-llvm40-gep_type_iterator-has-no-operator.patch -> + 0013-llvm40-gep_type_iterator-has-no-operator.patch + +------------------------------------------------------------------- +Mon Jan 15 07:49:05 UTC 2018 - jslaby@suse.com + +- change "env python" to "python3" in tests, so that we can build and + depend on py3 only + +------------------------------------------------------------------- +Mon Jan 8 07:18:25 UTC 2018 - jslaby@suse.com + +- add python3-setuptools BuildRequires, so that we have pkg_resources + for tests + +------------------------------------------------------------------- +Fri Nov 17 17:01:38 UTC 2017 - jslaby@suse.com + +- Update to version 1.4.0+20171026: + * [cmake]Fix detection of non-standard path for tcmalloc + * fixing huge allocation size constant to be unsigned + * [travis] build metaSMT with C++11 + * [travis] add a workaround to keep Travis alive when running tests for metaSMT-CVC4 (which needs around 10m for one specific test case) + * [travis] update scripts to additionally test CVC4 and Yices2 + * [cmake] detect available metaSMT backends using a pre-defined flag and raise compile flags accordingly + * add support for CVC4 and Yices2 via metaSMT + * Fixed assert in BFSSearcher that does not hold as part of interleaved searcher + * Removed unnecessary and redundant variable +- removed + * 0001-errno-define-__errno_location.patch + * 0001-test-DirSeek-make-it-XFAIL-temporarily.patch +- added + * 0001-Fix-generation-of-expressions-from-constant-sequenti.patch + * 0002-Fix-getelementptr-for-array-or-vector-indices.patch + * 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch + * 0004-Provide-errno-independent-of-CTYPE_EXTERNALS-being-d.patch + * 0005-Track-errno-correctly.patch + * 0006-Declare-klee_get_errno-and-remove-local-declarations.patch + * 0007-Add-support-for-modelling-errno_location.patch + * 0008-Cleanup-test-cases.patch + * 0009-test-fix-Feature-BFSSearcherAndDFSSearcherInterleave.patch + * 0012-llvm40-gep_type_iterator-has-no-operator.patch + * 0013-llvm38-test-change-some-tests.patch + +------------------------------------------------------------------- +Tue Oct 10 12:45:08 UTC 2017 - jslaby@suse.com + +- Update to version 1.4.0+20171009: + * Added support for hiding command-line options + * Removed "llvm::" and reformatting in CmdLineOptions.cpp + * Remove unnecessary null pointer checks + * Removed dead link, fixes #754 + * [CMake] Fix initialisation order of `KLEE_COMPONENT_*` and `KLEE_SOLVER_LIBRARIES` variables. The code to add `NDEBUG` to `KLEE_COMPONENT_CXX_DEFINES` did so before initialisation and would be silently overwritten. + * [CMake] Report the value of some important variables during configure to aid debugging. + * Silenced some warnings about unused variables when assertions are disabled. + * Remove Autoconf/Makefile build system and adjust the TravisCI configuration, TravisCI scripts and Dockerfile build appropriately. + * Fix TravisCI `METASMT_DEFAULT` setting. + * [CMake] Fix bug when doing non-assert builds. + * [CMake] Add global clean target `clean_all`. Fixes #718. + * [CMake] Add `clean_doxygen` rule to clean up doxygen build tree and add this as a dependency of `clean_all`. + * enforce c++11 + * Removed the word 'unsigned' from integer overflow error messages + * Silenced warnings on comparison of integers of different signs in TreeStreamTest + * Fixed initialization of distance to uncovered instructions when KLEE relies on default searchers +- removed: + * 0004-cmake-expand-library-dependencies-with-USE_CMAKE_FIN.patch +- renamed: + * 0005-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch -> + 0004-llvm37-handle-getRegisteredOptions.patch + * 0006-llvm-make-KLEE-compile-against-LLVM-3.8.patch -> + 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch + * 0007-llvm-make-KLEE-compile-against-LLVM-3.9.patch -> + 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch + * 0008-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch -> + 0007-llvm40-handle-different-header-names.patch + * 0009-llvm40-handle-different-header-names.patch -> + 0007-llvm40-handle-different-header-names.patch + * 0010-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch -> + 0008-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + * 0011-llvm40-errorOr-and-similar.patch -> + 0009-llvm40-errorOr-and-similar.patch + * 0012-llvm-use-chrono-helpers-from-LLVM-4.0.patch -> + 0010-llvm-use-chrono-helpers-from-LLVM-4.0.patch + * 0013-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch -> + 0011-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch + +------------------------------------------------------------------- +Thu Aug 17 12:05:26 UTC 2017 - jslaby@suse.com + +- Update to version 1.4.0+20170811: + * Removing flaky test Vararg.c from Darwin build until we find a proper fix + * Fixed typos in comments related to vararg support. + * llvm: don't use clEnumValEnd for LLVM 4.0 + * llvm: get rid of static_casts from iterators + * llvm37: do not copy DILocation to getDSPIPath + * Added location info for external calls and improved a message. + * llvm37: introduce type for PassManager + * move module loading into external function + * Corrected comment of Z3Solver class + * Added caching of Homebrew downloads + * Use assembly line for printing debug information + * Fixes bug in TreeStreamWriter::write reported by @gladtbx in #562. Also removes commented out code from that function. + * Implement basic support for vectorized instructions. + * Added some unit tests for TreeStream: one testing some basic behaviour, the other a regression test for #562 + * Core: TimingSolver, use TimerStatIncrementer + * Replace assertions of types on LLVM instructions in the Executor with a pass that checks these assertions. This improves several things. + * Switching version to 1.4.0 + * Release notes for 1.4.0 + * Remove support for LLVM < 3.4 + * Updated test cases to reflect removal of LLVM 2.9 + * Cleanup Travis builder + * Remove klee-gcc + * Remove LLVM 2.9 from Makefiles + * [CMake] Fix bug where the runtime build system would not rebuild bitcode archive/modules when the list of source files that constitute it changes. + * [CMake] Add a sanity check to the runtime build system so that we provide a better error message (and stop earlier) when no C source files are found. + * llvm: get rid of static_casts from iterators (take 2) + * more portable shebangs + * Moved klee_choose from klee-libc to KLEE intrinsics. + * Re-enable parts of `FloatingPointOps.ll`. The message about failures doesn't seem relevant anymore given that LLVM 3.4 is the minimum version KLEE supports. Also do minor clean up. This was spotted by @andreamattavelli. + * Added the const qualifier to the keys in the constantMap + * This commit simply moves evalConstant to ExecutorUtil (where evalConstantExpr also resides), as suggested by an old comment. + * [CMake] Fix bug where we would inherit LLVM's `-DNDEBUG` define when LLVM was built without assertions. This prevented `ENABLE_KLEE_ASSERTS` from working correctly. + * [CMake] Emit warning when mixing assert and non assert builds. + * Cleanup tests for last LLVM 2.9 references + * Added regression test for bug reported by @kren1 in #262 + * This reverts incorrect patch https://github.com/klee/klee/commit/db29a0bba74b672cdf4b8fef4d94ffa6ab845e6d __fprintf_chk has a different prototype than fprintf + * Now that LLVM 2.9 is gone, we can use cl::bits instead of cl::list + * [CMake] Refactor STP detection and change the default value of `ENABLE_SOLVER_STP` to be set dynamically based on whether STP is available. Previously the default was always off. + * [CMake] Refactor Z3 detection and change the default value of `ENABLE_SOLVER_Z3` to be set dynamically based on whether Z3 is available. Previously the default was always off. + * [CMake] Add `ENABLE_ZLIB` option to control whether KLEE uses zlib. The default is `ON` if zlib is found on first configure and `OFF` if zlib is not found on first configure. + * [CMake] Change the default value of `ENABLE_SOLVER_METASMT` to be set dynamically based on whether MetaSMT is available. Previously the default was always off. + * [TravisCI] Make sure when building with CMake that only the solvers requested get used. + * Modified Travis-CI script to compile STP with BOOST support + * Fixed script for STP in Travis-CI: Build now exits on errors + * Added another variant of printFileLine in KInstruction that returns the location as a string. Also added const qualifier to the printFileLine functions + * Added an optional KInstruction* argument to evalConstant and evalConstantExpr which allows us to print the location associated with the constant in any error messages. Added a test case for the unsupported features for taking the address of a label, which exercises the patch. + * Fix build for FreeBSD. + * Fixed test case counter: Previously the number of test cases generated by KLEE was always incremented, even if a symbolic solution was not found. + * Removed merging searchers + * Added checks for div/mod by zero and overshifts in constant expressions. Such div/mod by zero expressions would previously crash KLEE. Added two test cases, one for div/mod by zero, the other for overshift. This fixes the bug reported in #268. + * Untabify this file, which was using a mix of spaces and tabs for alignment. + * Fixed a compiler warning (unused variable) + * Fixed a bug causing KLEE to generate files with no permissions bits set. This was introduced when we added the --readable-posix-inputs option. + * Added a basic test for klee-replay +- reshuffle with patches + * A 0001-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch + * A 0002-llvm-make-KLEE-compile-against-LLVM-3.7.patch + * A 0003-test-add-versions-of-some-tests-for-LLVM-3.7.patch + * A 0004-cmake-expand-library-dependencies-with-USE_CMAKE_FIN.patch + * A 0005-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch + * A 0006-llvm-make-KLEE-compile-against-LLVM-3.8.patch + * A 0007-llvm-make-KLEE-compile-against-LLVM-3.9.patch + * A 0008-llvm37-handle-GetElementPtrInst-Create-s-new-paramet.patch + * D 0001-llvm-don-t-use-clEnumValEnd-for-LLVM-4.0.patch + * D 0002-llvm-get-rid-of-static_casts-from-iterators.patch + * D 0003-Core-TimingSolver-use-WallTimer.patch + * D 0004-llvm-make-KLEE-compile-against-LLVM-3.7.patch + * D 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch + * D 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch + * D 0007-test-add-versions-of-some-tests-for-LLVM-3.8.patch + * D 0008-travis-CI-add-LLVM-3.8-build-tests.patch + +------------------------------------------------------------------- +Tue Jun 27 08:43:06 UTC 2017 - jslaby@suse.com + +- switch to python 3 + +------------------------------------------------------------------- +Thu Jun 08 08:48:58 UTC 2017 - jslaby@suse.com + +- Build against LLVM 4 +- Update to version 1.3.0+20170607: + * Fix test failure on systems with libstdc++ corresponding to gcc7. + * llvm: rename ExitOnError to OptExitOnError + * Prevent test failure when realloc fails in test/Feature/Realloc.c +- added patches: + 0001-llvm-don-t-use-clEnumValEnd-for-LLVM-4.0.patch + 0002-llvm-get-rid-of-static_casts-from-iterators.patch + 0003-Core-TimingSolver-use-WallTimer.patch + 0004-llvm-make-KLEE-compile-against-LLVM-3.7.patch + 0005-llvm-make-KLEE-compile-against-LLVM-3.8.patch + 0006-llvm-make-KLEE-compile-against-LLVM-3.9.patch + 0007-test-add-versions-of-some-tests-for-LLVM-3.8.patch + 0008-travis-CI-add-LLVM-3.8-build-tests.patch + 0009-llvm40-handle-different-header-names.patch + 0010-llvm-APFloat-members-are-functions-in-LLVM-4.0.patch + 0011-llvm40-errorOr-and-similar.patch + 0012-llvm-use-chrono-helpers-from-LLVM-4.0.patch + 0013-llvm-PointerType-is-not-SequentialType-in-LLVM-4.patch +- removed patches (renamed to the above): + 0001-test-add-versions-of-some-tests-for-LLVM-3.8.patch + 0002-Make-KLEE-compile-against-LLVM-3.7.patch + 0003-Make-KLEE-compile-against-LLVM-3.8.patch + +------------------------------------------------------------------- +Mon Jun 05 07:45:51 UTC 2017 - jslaby@suse.com + +- Update to version 1.3.0+20170602: + * use METASMT_REQUIRE_RTTI flag to decide whether we need RTTI + * [travis] add environment variable METASMT_BOOST_VERSION to control the boost version used by metaSMT and test it with the combination LLVM-2.9 + metaSMT + * [CMake] change WARNING to FATAL_ERROR when building with a non-RTTI LLVM version and a metaSMT version that requires RTTI + * [TravisCI] Try to unbreak the build against upstream STP. + * Remove redundant KLEE prefix while logging + * llvm: make KLEE compile against LLVM 3.5 and 3.6 + * travis CI: add LLVM 3.5 and 3.6 tests + * Rearchitect ExternalDispatcher + * gitignore build + * [Z3] Support another solver failure reason that Z3 might give. I'm going to guess it means timeout but I'm not 100% sure about this. + * [Z3] Add assertions in Z3 builder to catch underflow with bad widths. + * [Z3] Move the `dump()` methods of the Z3NodeHandle<> specializations into `Z3Builder.cpp` so they can be called from in gdb. + * Refactor file opening code out of `main.cpp` and into `klee_open_output_file()` function so that it can be used by the Z3Solver. + * [Z3] Add the `-debug-z3-dump-queries=` command line option. This is useful for getting access to the constraints being stored in the Z3 solver in the SMT-LIBv2.5 format. + * [Z3] Add option to manually validate Z3 models. + * [Z3] Implement API logging. + * [Z3] In `getConstraintLog()` use a separate builder from that of the solver. This is to avoid tampering with the cache of the builder the solver is using. + * [Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`. + * [Z3] Add `-debug-z3-verbosity=` option which behaves like Z3's `-v:` option. This lets us see what Z3 is doing execution (e.g. which tactic is being applied) which is very useful for debugging. + * [Z3] Remove unused include. + * replace handleMetaSMT() with klee::createMetaSMTSolver() and move it into MetaSMTSolver.cpp so that the backend headers only need to be included once there + * hide backend solver declarations from public include +- remove 0001-Make-KLEE-compile-against-LLVM-3.5-and-3.6.patch + It is upstream already. + +------------------------------------------------------------------- +Wed Apr 26 09:18:55 UTC 2017 - jslaby@suse.com + +- Update to version 1.3.0+20170409: + * [TravisCI] Check if `METASMT_VERSION` is set and abort if it is not set. Also exit if any of the commands in `.travis/metaSMT.sh` fail. + * [TravisCI] Try to unbreak the metaSMT build. + * [TravisCI] Try unbreaking the TravisCI metaSMT build. Copying across the `cmake` directory breaks KLEE's CMake build. + * [CMake] Try to fix bug reported by #633. + * [CMake] Fix #631 + * [CMake] When supported pass `USES_TERMINAL` argument to `ExternalProject_Add_Step()` so that when using Ninja the output of the bitcode build system is shown immediately. + * [CMake] Add the `clean_runtime` top level target to provide an easy way to clean the runtime build. + * [Docker] Unbreak build. + * [TravisCI] Make handling of `TRAVIS_OS_NAME` more robust by not assuming that its value not being `linux` implies `osx`. + * test: lit, add geq/lt-llvm- configs + * [NFC] Reindent `test/lit.cfg` and add vim mode line to use right indentation and syntax highlighting. + * [travis] fix a git submodule failure of metaSMT + * [CMake] Don't redownload FileCheck.cpp if it exists + * Removed unused variable 'fake_object' in MemoryObject + +------------------------------------------------------------------- +Tue Mar 28 13:43:30 UTC 2017 - jslaby@suse.com + +- Update to version 1.3.0+20170328: + * runtime: POSIX, make it compile with glibc 2.25 + * [Lit] Add system information (linux/darwim) to LIT configuration. Added 'not-*' features that exist if target operating system does not match a list of know operating systems. + * Fix test case for OSX: only weak aliases are supported on darwin Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin' + * test: fix 'not' build + * test: POSIX, stop FD_Fail to fail + * runtime: POSIX, check path prior dereference + * [travis] use a proper version of metaSMT via environment variable METASMT_VERSION + * [travis] build metaSMT without C++11 + * remove special handling of metaSMT_CXXFLAGS (unnecessary now as we use a fixed version of metaSMT with this flag being properly set) + * [WIP] Fix bug where stats would not be updated on early exit caused by finding a bug with the `-exit-on-error` option enabled. + * Replace `llvm:errs()` with `klee_error()` as suggested by @andreamattavelli + * Add test case to check that on early exits stats are flushed + * Add `AssignmentValidatingSolver`. It's purpose is to check any computed assignments against the corresponding `Query` object and check the assignment evaluates correctly. + * [CMake] Unbreak build due to not adding AssignmentValidatingSolver.cpp to list of source files. + * [Travis-CI] Refactored Z3 in its own script + * [Travis-CI] Added support for macOS build +- enable checking of the result (%check section), only on x86_64 +- add some patches + * 0001-errno-define-__errno_location.patch + * 0001-test-DirSeek-make-it-XFAIL-temporarily.patch + * 0001-test-add-versions-of-some-tests-for-LLVM-3.8.patch +- renamed patches + * 0005-Make-KLEE-compile-against-LLVM-3.7.patch + -> 0002-Make-KLEE-compile-against-LLVM-3.7.patch + * 0006-Make-KLEE-compile-against-LLVM-3.8.patch + -> 0003-Make-KLEE-compile-against-LLVM-3.8.patch +- deleted patches (they are upstream) + * 0001-runtime-POSIX-make-it-compile-with-glibc-2.25.patch + * 0002-Fix-compiler-warning.patch + * 0004-Cleanup-removed-unneccessary-bools.patch + * 0007-fix-compilation-on-LLVM-3.8-after-rebase-to-master.patch + +------------------------------------------------------------------- +Wed Mar 15 12:57:25 UTC 2017 - jslaby@suse.com + +- add 0001-runtime-POSIX-make-it-compile-with-glibc-2.25.patch +- Update to version 1.3.0+20170307: + * klee: remove use of deprecated 'register' + * Makefile: change -std-compile-opts to -O3 + * CommandLine: do not copy list in optionIsSet + * Teach KLEE to respect the requested memory alignment of globals and stack variables when possible. + * llvm: stop using global context + * Module: simplify is_object checks + * convert iterators using static_cast + * Core: MCJIT functions need unique names + * Added new option --warnings-only-to-file which causes warnings to be written to warnings.txt only. Disabled by default. + * Updated test cases that check warning messages. + * Core: explicitly create CallSite from Instruction + * fix for PathOS.id + * Using klee_message instead of llvm:errs + * Moved printFileLine() to be part of KInstruction + * test: POSIX/DirSeek, cleanup + * test: ConstantExpr, fix bogus test + +------------------------------------------------------------------- +Thu Mar 2 14:11:06 UTC 2017 - jslaby@suse.com + +- enable uclibc & POSIX runtime +- add some %doc files + +------------------------------------------------------------------- +Wed Feb 22 10:36:55 UTC 2017 - jslaby@suse.com + +- Update to version 1.3.0+20170221: + * Fix `Feature/MemoryLimit.c` test when building KLEE with ASan. + * [TravisCI] Modify TravisCI/Docker build scripts to support doing ASan/UBSan builds of KLEE. + * Fix the Autoconf/Makefile build system when building with coverage flags. + * Teach both build systems to pass the user provided CXXFLAGS and CFLAGS when using the native compiler in system tests. + * In legacy build system fix building libkleeRuntest when building with ASan. + * Increased the type size for the stop-after-n-instructions option to avoid too strict limitations + * Revert "Increased the type size for the stop-after-n-instructions option to a…" + * Silenced two "control may reach end of non-void function [-Wreturn-type]" compiler warnings, one by adding an assert, and the other by refactoring the choose() function. + * Removing unused lib/SMT directory + * Added error message when STP fails to fork. + * ReadExpr::create() was missing an opportunity to constant fold when handling constant arrays. + * Added unit tests for ReadExpr::create() to check that constant folding is correctly applied + * Added pre/post conditions as assertions + * Fixed assertion invocation: We were invoking bits64::truncateToNBits with a width greater than 64 + * Refactoring code to improve readability by using UINT32/64_C macros + * Fix linker compatibility under macOS + * Increased the type size for the stop-after-n-instructions option to avoid too strict limitations (LLVM >= 3.0) + * Silenced warning: comparison of integers of different signs ('const int' and 'const unsigned long long') + * Add test case that causes an assertion failure in `klee::getDirectCallTarget(llvm::CallSite)`. + * Teach `klee::getDirectCallTarget()` to resolve weak aliases. This is controlled by a new parameter `moduleIsFullyLinked`. When true the linkage type of a weak alias is ignored. It is legal to do this when the module is fully linked because there won't be another function that could override the weak alias. + * fix metaSMT version + +------------------------------------------------------------------- +Mon Feb 13 12:06:09 UTC 2017 - jslaby@suse.com + +- Update to version 1.3.0+20170211: + * [cmake] add PATH_SUFFIXES needed to find z3 on Fedora + * test: fix broken Vararg test + * [CMake] More widely available rebuilding for runtimes +- switch to llvm 3.8 + +------------------------------------------------------------------- +Fri Jan 27 12:43:32 UTC 2017 - jslaby@suse.com + +- Update to version 1.3.0+20170118: + * Typo fix when compiling with LLVM 3.5 and above + * [TravisCI] Fix bug where TravisCI build scripts would carry on executing even though configure/build failed. This due to using the `&&` operator which means failure of commands to execute in this compound statement will not trigger the script to exit as requested by `set -e`. + * [TravisCI] Remove `set +e` commands so that when running tests we fail fast rather than continuing to run the tests (due to `set -e` at the beginning of the script). + * [TravisCI] When building with the old build system move back to the root of the build tree after doing the hack the generate the lit configuration files. + * CMake: Fixed the LLVM version regex + * [CMake] Fix linker warning about mixed linking modes when LLVM was built with `-fvisibility-inlines-hidden`. + * Fix -Wformat warnings emitted by Apple Clang (800.0.42.1). + * rerun lit tests for non-default metaSMT backends + * Changed preferred permissions from 0622 to the more standard 0644. + * Fix two issues with AC_LINK_IFELSE for metaSMT: + * tests: Added substitution for llvm-ar + * Write tests to test `libkleeRuntest`. The `replay_posix_runtime.c` test is marked XFAIL because there is a bug in the implementation of `libkleeRuntest`. + * Fix bug reported privately by @danielschemmel . + * Change how error handling is done in libkleeRuntest. + * [CMake] Rename "integrationtests" to "systemtests". + * Rename old build system targets so that + * Remove undocumented and unused `check-local`, `check-dg` and `check-lit` targets from Autoconf/Makefile build system. Having these around just confuses things. + * [CMake] Only add dependencies to `check` if the target is enabled. + * [CMake] If CMP0037 policy is available set it to NEW so that we disallow using reserved target names. + * [CMake] Remove `ENABLE_TESTS` CMake cache option. + +------------------------------------------------------------------- +Thu Dec 15 10:30:23 UTC 2016 - jslaby@suse.com + +- Update to version 1.3.0+20161210: + * Fixing current version of STP in Dockerfile (see #505) to 2.1.2 + * Switched to STP 2.1.2 on Travis CI builds + * Increasing version to 1.3.0 + * Release notes for 1.3.0 + * Remove support for reporting the approximate git tag. + * Added among the external calls that we model + * CMake: support LLVMCC.ExtraFlags + * Fixed the issue of klee-stats not being copied to bin/ + * [TravisCI] Fix the list of available configuration environment variables. + * [TravisCI] Clean up the configuration matrix. + * [CMake] Fix bug in the Makefile bitcode build system where the runtime would not recompile if the LLVM C compiler flags changed. This could happen if the user did something like + * [CMake] Fix bug in the Makefile bitcode build system where the runtime would not recompile if the `Makefile.cmake.bitcode.rules` file changed. + * [CMake] Fix bug where if KLEE was built with `ENABLE_TCMALLOC` and then re-configured with `ENABLE_TCMALLOC` set to OFF then `klee/Config/config.h` was not correctly re-generated. + +------------------------------------------------------------------- +Wed Nov 30 09:03:48 UTC 2016 - jslaby@suse.com + +- Update to version 1.0.0+20161129: + * [CMake] Add missing dependencies reported in #507. + * [CMake] Fix link order of LLVM libraries and required system libraries. + * [CMake] Add another missing LLVM component dependency for `kleeModule`. + * [CMake] Fix determining the system libraries needed by LLVM from `llvm-config` when using LLVM 3.5 and newer. + * [CMake] Fix bug where the wrong path is checked for when checking to see if we can find klee-uclibc's C library. + * [CMake] Fix some indentation issues. + * Renamed .pc to .kquery (kleaver query) + * Fix bug in implementation of `NotExpr`. It should not implement `compareContents()`. + * Remove default implementation of `Expr::compareContents(const Expr&)` and make it a pure virtual method. Also make it protected rather than public because it is an implementation detail of `Expr::compare()`. + * Clean up `Expr::compare()` interface by +- remove 0001-lib-Module-needs-codegen.patch + +------------------------------------------------------------------- +Mon Nov 21 12:54:44 UTC 2016 - jslaby@suse.com + +- Update to version 20161121: + * [CMake] Implement install of the kleeRuntest target. + * [CMake] Fix the build when `-DBUILD_SHARED_LIBS=ON` is passed. This fixes issue #507. + +------------------------------------------------------------------- +Sun Nov 20 19:26:50 UTC 2016 - jslaby@suse.com + +- remove proper-shared-libs.patch +- add 0001-lib-Module-needs-codegen.patch +- Update to version 20161119: + * add nicer error messages for --use-merge and add explanation why it currently cannot be used with random-path + * Fix BFS searcher + * [CMake] Re-express LLVM and KLEE library dependencies as transitive dependencies on KLEE's libraries rather than on the final binaries. This is better because it means we can build other tools that use KLEE's libraries and not need to express the needed LLVM dependencies. + * [CMake] Remove use of tabs in `CMakeLists.txt` files. + * [CMake] Document implicit `STP_DIR` and `metaSMT_DIR` options. + * Documented the level at which BFS operates in KLEE, as part of --help + * Remove option --randomize-fork. If someone needs this, the right way is to implement it in the solver. + * [CMake] Remove unneeded dependency declarations for the unit tests. These were changes that I forgot to make in dda296e09ee53ed85ccf1c3f08e7e809adce612e . + * [CMake] Fix the old Autoconf/Makefile build system files in source tree interfering with CMake build. + +------------------------------------------------------------------- +Fri Nov 18 14:55:02 UTC 2016 - jslaby@suse.com + +- switch to cmake +- Update to version 20161117: + * remove mimic_stp option and the associated ITE chain construction for shift operators + * When building KLEE with the sanitizers make sure the runtime is not built with them because KLEE can't handle this. + * Use newer trusty-based Travis CI (#452) + * Fix `-Wmisleading-indentation` warning and also correctly set the `dirty` flag if we remove `llvm.trap` from the module. + * remove outdated FIXME (metaSMT-Z3 implements assumption via push/pop) + * change signature of runAndGetCex() to match runAndGetCexForked() + * move the query creation part into runAndGetCex() (to be consistent with runAndGetCexForked()) + * upgrade to boolector-2.2.0 & remove the no longer needed aux array vector + * update comments + * apply clang-format + * Adds support for Darwin platform in RaiseAsm pass + * Implement a CMake based build system for KLEE. + * Add the Dockerfile to `.dockerignore` so that changes the Dockerfile don't trigger unnecessary rebuilds. Also make the Dockerfile ignore Vim source files anywhere in the tree. + * [CMake] Report git revision information if available. + * [cmake] Build with newer JIT (for LLVM >= 3.6) + +------------------------------------------------------------------- +Fri Sep 30 06:29:04 UTC 2016 - jslaby@suse.com + +- Update to version 20160929: + * Fixed the description of -posix-runtime option + * configure: add option to enable timestamping + * configure: run AutoRegen.sh + * Fix bug in `AssignmentEvaluator` where NotOptimizedExpr would not (#466) +- remove 0001-configure-add-option-to-enable-timestamping.patch: upstream +- remove 0002-configure-run-AutoRegen.sh.patch: upstream + +------------------------------------------------------------------- +Thu Sep 29 08:29:04 UTC 2016 - jslaby@suse.com + +- add 0001-configure-add-option-to-enable-timestamping.patch +- add 0002-configure-run-AutoRegen.sh.patch +- remove no_date_time.patch + +------------------------------------------------------------------- +Thu Sep 29 07:21:47 UTC 2016 - jslaby@suse.com + +- Update to version 20160926: + * Extended support for assembler raising + * Check the existence of the entry point during the initialization of the POSIX runtime. If the check fails, exit with an error. (#457) + * Clang-format ``ConstructSolverChain.cpp`` + * Add ``-debug-cross-check-core-solver`` option to allow cross-checking with another solver. For example the core solver can be STP and the cross checking solver can be Z3. + * Correct out of date comments for some of the klee error handling functions. + * Rename `-debug-cross-check-core-solver` option to `-debug-crosscheck-core-solver` as requested by Cristian + * Avoid internalization of non-standard entry point (i.e. not the main function) (#455) + * Modified logging information to steer the usage of klee_message, klee_warning, and klee_error +- remove Executor-skip-empty-asm-instead-of-abort.patch: upstream +- remove Executor-do-not-crash-on-non-sized-globals.patch: upstream + +------------------------------------------------------------------- +Mon Aug 1 17:01:41 UTC 2016 - jslaby@suse.com + +- Add gperftools-devel, libacl-devel, libcap-devel, libselinux-devel + to BuildRequires. It allows for more features. + +------------------------------------------------------------------- +Tue May 31 08:20:56 UTC 2016 - jslaby@suse.com + +- update to 20160528 + * Fixed an incorrect read() invocation and missing includes for FD_Fail2.c + * Improved help message for POSIX environment options. + * add entry for llvm-2.9 and z3 + * add include in Z3Solver.cpp (did not compile with llvm-2.9) + * Split creation of symbolic files and stdin in two distinct options + * Fixed bug #375 in Kleaver's parser + * Allow relocation of installed klee tree + * Modified -debug-print-instructions to allow to write directly on log file. + * Add cmake 2.8.11 as additional dependency + +------------------------------------------------------------------- +Fri Apr 29 12:02:37 UTC 2016 - jslaby@suse.com + +- Executor-skip-empty-asm-instead-of-abort.patch: add + +------------------------------------------------------------------- +Thu Apr 28 13:09:08 UTC 2016 - jslaby@suse.com + +- Executor-do-not-crash-on-non-sized-globals.patch: add + +------------------------------------------------------------------- +Mon Apr 25 18:01:52 UTC 2016 - jslaby@suse.com + +- update to 20160419 + +------------------------------------------------------------------- +Fri Mar 11 10:15:10 UTC 2016 - jslaby@suse.com + +- build against llvm34-klee and do not rebuild llvm +- add proper-shared-libs.patch + +------------------------------------------------------------------- +Wed Mar 9 15:42:23 UTC 2016 - jslaby@suse.com + +- update to 20160306 + +------------------------------------------------------------------- +Fri Nov 27 09:44:56 UTC 2015 - jslaby@suse.com + +- update to 20151113 + +------------------------------------------------------------------- +Fri Sep 4 09:20:13 UTC 2015 - jslaby@suse.com + +- use date for filename + +------------------------------------------------------------------- +Fri Sep 4 08:18:12 UTC 2015 - jslaby@suse.com + +- add: no_date_time.patch + +------------------------------------------------------------------- +Thu Sep 3 18:29:29 UTC 2015 - jslaby@suse.com + +- update to 1440176974 +- use llvm 3.4 + +------------------------------------------------------------------- +Thu Nov 13 12:22:18 UTC 2014 - jslaby@suse.com + +- initial commit + diff --git a/klee.obsinfo b/klee.obsinfo new file mode 100644 index 0000000..cebefba --- /dev/null +++ b/klee.obsinfo @@ -0,0 +1,4 @@ +name: klee +version: 3.1+20240614 +mtime: 1718389371 +commit: 26632f1d883e1343a23fd200d2dde070707b294d diff --git a/klee.spec b/klee.spec new file mode 100644 index 0000000..1e5f94e --- /dev/null +++ b/klee.spec @@ -0,0 +1,147 @@ +# +# spec file for package klee +# +# Copyright (c) 2024 SUSE LLC +# +# All modifications and additions to the file contributed by third parties +# remain the property of their copyright owners, unless otherwise agreed +# upon. The license for this file, and modifications and additions to the +# file, is the same license as for the pristine package itself (unless the +# license for the pristine package is not an Open Source License, in which +# case the license is the MIT License). An "Open Source License" is a +# license that conforms to the Open Source Definition (Version 1.9) +# published by the Open Source Initiative. + +# Please submit bugfixes or comments via https://bugs.opensuse.org/ +# + + +%define llvm_version 16 + +%ifarch x86_64 +%define with_uclibc 1 +%else +%define with_uclibc 0 +%endif + +%define runtime_variants Debug,Debug+Asserts,Release,Release+Asserts,Release+Debug,Release+Debug+Asserts + +Name: klee +Summary: LLVM Execution Engine +License: NCSA +Group: Development/Languages/Other +Version: 3.1+20240614 +Release: 0 +URL: http://klee.github.io/ +Source0: %{name}-%{version}.tar.xz +Source1: %{name}-rpmlintrc +Source2: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version}.0.0/llvm/utils/not/not.cpp +Source3: https://raw.githubusercontent.com/llvm/llvm-project/llvmorg-%{llvm_version}.0.0/llvm/utils/FileCheck/FileCheck.cpp + +BuildRequires: clang%{llvm_version} +BuildRequires: cmake +BuildRequires: gperftools-devel +%if %{with_uclibc} +BuildRequires: klee-uclibc-devel-static(llvm%{llvm_version}) +%endif +BuildRequires: libacl-devel +BuildRequires: libcap-devel +BuildRequires: libselinux-devel +BuildRequires: llvm%{llvm_version}-devel +BuildRequires: ninja +BuildRequires: python3 +BuildRequires: python3-lit +BuildRequires: python3-setuptools +BuildRequires: python3-tabulate +# tests need sqlite3 +BuildRequires: sqlite3-devel +BuildRequires: stp-devel +BuildRequires: xz +BuildRequires: zlib-devel +# 32 bit doesn't build and won't be fixed +ExcludeArch: %{ix86} %{arm} + +%description +KLEE is a symbolic virtual machine built on top of the LLVM compiler +infrastructure, and available under the UIUC open source license. For more +information on what KLEE is and what it can do, see the OSDI 2008 paper. + +%prep +%autosetup -p1 + +mkdir -p build/test/ +cp %{SOURCE2} build/test/ +cp %{SOURCE3} build/test/ + +sed -i '1s@/usr/bin/env python3*@/usr/bin/python3@' \ + test/Concrete/ConcreteTest.py \ + tools/klee-stats/klee-stats \ + tools/klee-zesti/klee-zesti \ + tools/ktest-tool/ktest-tool + +%build +# Make _lto_cflags compatible with Clang. On some arches, it doesn't work. +%ifarch x86_64 %{ix86} ppc64le s390x +%define _lto_cflags "-flto=thin" +%else +%define _lto_cflags %{nil} +%endif +%define __builder ninja +# they use -DNDEBUG, but we cannot, hence setting CMAKE_C*_FLAGS +# SHARED libs do not work at all yet +%cmake \ + -DCMAKE_C_COMPILER=clang \ + -DCMAKE_CXX_COMPILER=clang++ \ + -DCMAKE_AR=%{_bindir}/llvm-ar \ + -DCMAKE_RANLIB=%{_bindir}/llvm-ranlib \ + -DENABLE_KLEE_ASSERTS=OFF \ + -DENABLE_DOXYGEN=OFF \ + -DENABLE_SOLVER_STP=ON \ + -DENABLE_TCMALLOC=ON \ + -DENABLE_UNIT_TESTS=OFF \ + -DENABLE_SYSTEM_TESTS=ON \ + -DCMAKE_C_FLAGS="%optflags" \ + -DCMAKE_CXX_FLAGS="%optflags" \ +%if %{with_uclibc} + -DENABLE_POSIX_RUNTIME=ON \ + -DENABLE_KLEE_UCLIBC=ON \ + -DKLEE_UCLIBC_PATH=%{_libdir}/klee-uclibc/ \ +%endif + -DBUILD_SHARED_LIBS:BOOL=OFF +%cmake_build + +%check +%ifarch x86_64 +cd build +ninja check +%endif + +%install +%cmake_install + +%post -p /sbin/ldconfig + +%postun -p /sbin/ldconfig + +%files +%defattr(-,root,root) +%doc NEWS README.md +%license LICENSE.TXT +%{_bindir}/kleaver +%{_bindir}/klee* +%{_bindir}/ktest-* +%{_includedir}/klee/ +%{_libdir}/libkleeRuntest.so* +%dir %{_libdir}/klee/ +%dir %{_libdir}/klee/runtime/ +%{_libdir}/klee/runtime/libkleeRuntimeFortify*_{%{runtime_variants}}.bca +%{_libdir}/klee/runtime/libkleeRuntimeFreestanding*_{%{runtime_variants}}.bca +%{_libdir}/klee/runtime/libkleeRuntimeIntrinsic*_{%{runtime_variants}}.bca +%{_libdir}/klee/runtime/libkleeRuntimeKLEELibc*_{%{runtime_variants}}.bca +%{_libdir}/klee/runtime/libkleeUBSan*_{%{runtime_variants}}.bca +%if %{with_uclibc} +%{_libdir}/klee/runtime/klee-uclibc.bca +%{_libdir}/klee/runtime/libkleeRuntimePOSIX*_{%{runtime_variants}}.bca +%endif + +%changelog diff --git a/not.cpp b/not.cpp new file mode 100644 index 0000000..920f3fc --- /dev/null +++ b/not.cpp @@ -0,0 +1,82 @@ +//===- not.cpp - The 'not' testing tool -----------------------------------===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// Usage: +// not cmd +// Will return true if cmd doesn't crash and returns false. +// not --crash cmd +// Will return true if cmd crashes (e.g. for testing crash reporting). + +#include "llvm/Support/Program.h" +#include "llvm/Support/WithColor.h" +#include "llvm/Support/raw_ostream.h" + +#ifdef _WIN32 +#include +#endif + +using namespace llvm; + +int main(int argc, const char **argv) { + bool ExpectCrash = false; + + ++argv; + --argc; + + if (argc > 0 && StringRef(argv[0]) == "--crash") { + ++argv; + --argc; + ExpectCrash = true; + + // Crash is expected, so disable crash report and symbolization to reduce + // output and avoid potentially slow symbolization. +#ifdef _WIN32 + SetEnvironmentVariableA("LLVM_DISABLE_CRASH_REPORT", "1"); + SetEnvironmentVariableA("LLVM_DISABLE_SYMBOLIZATION", "1"); +#else + setenv("LLVM_DISABLE_CRASH_REPORT", "1", 0); + setenv("LLVM_DISABLE_SYMBOLIZATION", "1", 0); +#endif + } + + if (argc == 0) + return 1; + + auto Program = sys::findProgramByName(argv[0]); + if (!Program) { + WithColor::error() << "unable to find `" << argv[0] + << "' in PATH: " << Program.getError().message() << "\n"; + return 1; + } + + std::vector Argv; + Argv.reserve(argc); + for (int i = 0; i < argc; ++i) + Argv.push_back(argv[i]); + std::string ErrMsg; + int Result = + sys::ExecuteAndWait(*Program, Argv, std::nullopt, {}, 0, 0, &ErrMsg); +#ifdef _WIN32 + // Handle abort() in msvcrt -- It has exit code as 3. abort(), aka + // unreachable, should be recognized as a crash. However, some binaries use + // exit code 3 on non-crash failure paths, so only do this if we expect a + // crash. + if (ExpectCrash && Result == 3) + Result = -3; +#endif + if (Result < 0) { + WithColor::error() << ErrMsg << "\n"; + if (ExpectCrash) + return 0; + return 1; + } + + if (ExpectCrash) + return 1; + + return Result == 0; +}