Skip to content

Commit 2f251c8

Browse files
ladisginladisgin
committed
rebase
1 parent e6f9718 commit 2f251c8

File tree

8 files changed

+9
-224
lines changed

8 files changed

+9
-224
lines changed

‎CMakeLists.txt

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -671,17 +671,6 @@ include_directories("${CMAKE_SOURCE_DIR}/submodules/json/include")
671671
include_directories("${CMAKE_SOURCE_DIR}/submodules/optional/include")
672672

673673

674-
option(ENABLE_XML_ANNOTATION "Enable XML annotation" ON)
675-
676-
if (ENABLE_XML_ANNOTATION)
677-
message(STATUS "XML annotation is enabled")
678-
file(COPY "${CMAKE_SOURCE_DIR}/submodules/pugiconfig.hpp"
679-
DESTINATION "${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
680-
include_directories("${CMAKE_SOURCE_DIR}/submodules/pugixml/src")
681-
else()
682-
message(STATUS "XML annotation is disabled")
683-
set(ENABLE_XML_ANNOTATION 0)
684-
endif()
685674
# set(KLEE_INCLUDE_DIRS ${CMAKE_SOURCE_DIR}/include ${CMAKE_BINARY_DIR}/include)
686675

687676
################################################################################

‎include/klee/Config/config.h.cmin

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,4 @@ macro for that. That would simplify the C++ code. */
122122
/* Install directory for KLEE runtime */
123123
#define KLEE_INSTALL_RUNTIME_DIR "@KLEE_INSTALL_RUNTIME_DIR@"
124124

125-
/* Enable XML annotation parser */
126-
#define ENABLE_XML_ANNOTATION "@ENABLE_XML_ANNOTATION@"
127-
128125
#endif /* KLEE_CONFIG_H */

‎include/klee/Expr/SymbolicSource.h

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -359,8 +359,8 @@ class AlphaSource : public SymbolicSource {
359359
const unsigned index;
360360

361361
AlphaSource(unsigned _index) : index(_index) {}
362-
Kind getKind() const override { return Kind::Alpha; }
363-
virtual std::string getName() const override { return "alpha"; }
362+
[[nodiscard]] Kind getKind() const override { return Kind::Alpha; }
363+
[[nodiscard]] virtual std::string getName() const override { return "alpha"; }
364364

365365
static bool classof(const SymbolicSource *S) {
366366
return S->getKind() == Kind::Alpha;
@@ -406,16 +406,16 @@ class MockNaiveSource : public MockSource {
406406
unsigned _version)
407407
: MockSource(km, function), version(_version) {}
408408

409-
Kind getKind() const override { return Kind::MockNaive; }
410-
std::string getName() const override { return "mockNaive"; }
409+
[[nodiscard]] Kind getKind() const override { return Kind::MockNaive; }
410+
[[nodiscard]] std::string getName() const override { return "mockNaive"; }
411411

412412
static bool classof(const SymbolicSource *S) {
413413
return S->getKind() == Kind::MockNaive;
414414
}
415415

416416
unsigned computeHash() override;
417417

418-
int internalCompare(const SymbolicSource &b) const override;
418+
[[nodiscard]] int internalCompare(const SymbolicSource &b) const override;
419419
};
420420

421421
class MockDeterministicSource : public MockSource {
@@ -425,16 +425,16 @@ class MockDeterministicSource : public MockSource {
425425
MockDeterministicSource(const KModule *_km, const llvm::Function &_function,
426426
const std::vector<ref<Expr>> &_args);
427427

428-
Kind getKind() const override { return Kind::MockDeterministic; }
429-
std::string getName() const override { return "mockDeterministic"; }
428+
[[nodiscard]] Kind getKind() const override { return Kind::MockDeterministic; }
429+
[[nodiscard]] std::string getName() const override { return "mockDeterministic"; }
430430

431431
static bool classof(const SymbolicSource *S) {
432432
return S->getKind() == Kind::MockDeterministic;
433433
}
434434

435435
unsigned computeHash() override;
436436

437-
int internalCompare(const SymbolicSource &b) const override;
437+
[[nodiscard]] int internalCompare(const SymbolicSource &b) const override;
438438
};
439439

440440
} // namespace klee

‎lib/Expr/SourceBuilder.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,6 @@ SourceBuilder::mockDeterministic(const KModule *km,
106106
return r;
107107
}
108108

109-
110109
ref<SymbolicSource> SourceBuilder::alpha(int _index) {
111110
ref<SymbolicSource> r(new AlphaSource(_index));
112111
r->computeHash();

‎lib/Module/Annotation.cpp

Lines changed: 0 additions & 118 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,6 @@
66
#include <llvm/Support/raw_ostream.h>
77
#include <utility>
88

9-
#ifdef ENABLE_XML_ANNOTATION
10-
#include "pugixml.hpp"
11-
#endif
12-
139
namespace klee {
1410

1511
static inline std::string toLower(const std::string &str) {
@@ -241,107 +237,6 @@ AnnotationsMap parseAnnotationsJson(const json &annotationsJson) {
241237
return annotations;
242238
}
243239

244-
#ifdef ENABLE_XML_ANNOTATION
245-
246-
namespace annotationXml {
247-
248-
const std::map<std::string, Statement::Kind> StringToKindMap = {
249-
{"C_NULLDEREF", Statement::Kind::Deref},
250-
{"C_NULLRETURN", Statement::Kind::InitNull}};
251-
252-
inline Statement::Kind xmlTypeToKind(const std::string &str) {
253-
auto it = StringToKindMap.find(str);
254-
if (it != StringToKindMap.end()) {
255-
return it->second;
256-
}
257-
klee_message("Annotations: unknown xml type \"%s\"", str.c_str());
258-
return Statement::Kind::Unknown;
259-
}
260-
261-
const std::map<std::string, Statement::Property> xmlPropertyMap = {};
262-
263-
inline Statement::Property xmlTypeToProperty(const std::string &str) {
264-
auto it = xmlPropertyMap.find(str);
265-
if (it != xmlPropertyMap.end()) {
266-
return it->second;
267-
}
268-
return Statement::Property::Unknown;
269-
}
270-
271-
AnnotationsMap parseAnnotationsXml(const pugi::xml_document &annotationsXml,
272-
const llvm::Module *m) {
273-
AnnotationsMap result;
274-
for (pugi::xml_node rules : annotationsXml.child("RuleSet")) {
275-
for (pugi::xml_node customRule : rules) {
276-
for (pugi::xml_node keyword : customRule.child("Keywords")) {
277-
std::string name = keyword.attribute("name").value();
278-
std::string isRegex = keyword.attribute("isRegex").value();
279-
if (toLower(isRegex) == "true") {
280-
klee_warning("Annotation: regexp currently not implemented");
281-
continue;
282-
}
283-
std::string value = keyword.attribute("value").value();
284-
std::string type = keyword.attribute("type").value();
285-
std::string pairedTo = keyword.attribute("pairedTo").value();
286-
287-
llvm::Function *func = m->getFunction(name);
288-
if (!func) {
289-
continue;
290-
}
291-
292-
auto it = result.find(name);
293-
if (result.find(name) == result.end()) {
294-
Annotation newAnnotation;
295-
newAnnotation.functionName = name;
296-
newAnnotation.argsStatements =
297-
std::vector<std::vector<Statement::Ptr>>(func->arg_size());
298-
299-
result[name] = std::move(newAnnotation);
300-
it = result.find(name);
301-
}
302-
Annotation &curAnnotation = it->second;
303-
Statement::Kind curKind = xmlTypeToKind(type);
304-
305-
switch (curKind) {
306-
case Statement::Kind::InitNull: {
307-
curAnnotation.returnStatements.push_back(
308-
std::make_shared<Statement::InitNull>());
309-
break;
310-
}
311-
case Statement::Kind::Deref: {
312-
size_t i = 0;
313-
for (const auto &arg : func->args()) {
314-
if (arg.getType()->isPointerTy()) {
315-
curAnnotation.argsStatements[i].push_back(
316-
std::make_shared<Statement::Deref>());
317-
++i;
318-
}
319-
}
320-
break;
321-
}
322-
case Statement::Kind::AllocSource: {
323-
assert(false);
324-
}
325-
case Statement::Kind::Unknown:
326-
break;
327-
}
328-
329-
Statement::Property curProperty = xmlTypeToProperty(type);
330-
331-
switch (curProperty) {
332-
case Statement::Property::Deterministic:
333-
case Statement::Property::Noreturn:
334-
case Statement::Property::Unknown:
335-
break;
336-
}
337-
}
338-
}
339-
}
340-
return result;
341-
}
342-
} // namespace annotationXml
343-
#endif
344-
345240
AnnotationsMap parseAnnotations(const std::string &path,
346241
const llvm::Module *m) {
347242
if (path.empty()) {
@@ -351,20 +246,7 @@ AnnotationsMap parseAnnotations(const std::string &path,
351246
if (!annotationsFile.good()) {
352247
klee_error("Annotation: Opening %s failed.", path.c_str());
353248
}
354-
#ifdef ENABLE_XML_ANNOTATION
355-
if (toLower(std::filesystem::path(path).extension()) == ".xml") {
356-
357-
pugi::xml_document doc;
358-
pugi::xml_parse_result result = doc.load_file(path.c_str());
359-
if (!result) {
360-
klee_error("Annotation: Parsing XML %s failed.", path.c_str());
361-
}
362-
363-
return annotationXml::parseAnnotationsXml(doc, m);
364-
} else {
365-
#else
366249
{
367-
#endif
368250
json annotationsJson = json::parse(annotationsFile, nullptr, false);
369251
if (annotationsJson.is_discarded()) {
370252
klee_error("Annotation: Parsing JSON %s failed.", path.c_str());

‎submodules/pugiconfig.hpp

Lines changed: 0 additions & 81 deletions
This file was deleted.

‎submodules/pugixml

Submodule pugixml deleted from 980cf57

‎test/Feature/MockStrategies.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
// CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only.
1919

2020
// RUN: rm -rf %t.klee-out-4
21-
// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4
21+
// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHsECK-4
2222
// CHECK-4: KLEE: done: completed paths = 2
2323
// CHECK-4: KLEE: done: generated tests = 2
2424

0 commit comments

Comments
 (0)