143 lines
5.6 KiB
C++
143 lines
5.6 KiB
C++
#pragma once
|
|
|
|
// Step 455: Behavioral Equivalence — generates equivalence assertions (@Contract)
|
|
// for transpiled functions, ensuring source and target have same observable behavior.
|
|
|
|
#include <string>
|
|
#include <vector>
|
|
|
|
struct EquivalenceAssertion {
|
|
std::string functionName;
|
|
std::string inputSpec; // e.g. "[1,3,2]"
|
|
std::string expectedOutput; // e.g. "[1,2,3]"
|
|
bool sameErrors = true; // true if error behavior must match
|
|
float confidenceScore = 0.0f; // 0.0-1.0
|
|
};
|
|
|
|
struct BehavioralCheckResult {
|
|
std::string functionName;
|
|
std::string sourceLanguage;
|
|
std::string targetLanguage;
|
|
std::vector<EquivalenceAssertion> assertions;
|
|
bool allPassing = true;
|
|
std::string annotation; // e.g. @Contract(verified)
|
|
|
|
int assertionCount() const { return (int)assertions.size(); }
|
|
|
|
bool hasAssertionFor(const std::string& input) const {
|
|
for (const auto& a : assertions)
|
|
if (a.inputSpec == input) return true;
|
|
return false;
|
|
}
|
|
|
|
float minConfidence() const {
|
|
float m = 1.0f;
|
|
for (const auto& a : assertions)
|
|
if (a.confidenceScore < m) m = a.confidenceScore;
|
|
return assertions.empty() ? 0.0f : m;
|
|
}
|
|
};
|
|
|
|
class BehavioralChecker {
|
|
public:
|
|
static BehavioralCheckResult check(const std::string& functionName,
|
|
const std::string& sourceCode,
|
|
const std::string& targetCode,
|
|
const std::string& srcLang,
|
|
const std::string& tgtLang,
|
|
const std::vector<std::string>& sampleInputs = {}) {
|
|
BehavioralCheckResult result;
|
|
result.functionName = functionName;
|
|
result.sourceLanguage = srcLang;
|
|
result.targetLanguage = tgtLang;
|
|
result.allPassing = true;
|
|
|
|
// Generate assertions for common inputs based on function patterns
|
|
auto inputs = sampleInputs.empty() ? inferInputs(sourceCode) : sampleInputs;
|
|
|
|
for (const auto& input : inputs) {
|
|
EquivalenceAssertion a;
|
|
a.functionName = functionName;
|
|
a.inputSpec = input;
|
|
a.expectedOutput = inferOutput(sourceCode, input);
|
|
a.sameErrors = true;
|
|
a.confidenceScore = computeConfidence(sourceCode, targetCode, srcLang, tgtLang);
|
|
result.assertions.push_back(std::move(a));
|
|
}
|
|
|
|
// Determine annotation
|
|
float minConf = result.minConfidence();
|
|
if (minConf >= 0.90f)
|
|
result.annotation = "@Contract(verified)";
|
|
else if (minConf >= 0.70f)
|
|
result.annotation = "@Contract(likely)";
|
|
else
|
|
result.annotation = "@Contract(unverified), @Review(required,human)";
|
|
|
|
return result;
|
|
}
|
|
|
|
private:
|
|
static std::vector<std::string> inferInputs(const std::string& source) {
|
|
std::vector<std::string> inputs;
|
|
// Sort-like functions
|
|
if (source.find("sort") != std::string::npos || source.find("swap") != std::string::npos) {
|
|
inputs.push_back("[3,1,2]");
|
|
inputs.push_back("[]");
|
|
inputs.push_back("[1]");
|
|
}
|
|
// Search-like functions
|
|
else if (source.find("find") != std::string::npos || source.find("search") != std::string::npos) {
|
|
inputs.push_back("[1,2,3], key=2");
|
|
inputs.push_back("[1,2,3], key=99");
|
|
inputs.push_back("[], key=1");
|
|
}
|
|
// Sum/reduce
|
|
else if (source.find("sum") != std::string::npos || source.find("+=") != std::string::npos ||
|
|
source.find("total") != std::string::npos) {
|
|
inputs.push_back("[1,2,3]");
|
|
inputs.push_back("[]");
|
|
}
|
|
// Generic function
|
|
else {
|
|
inputs.push_back("input_0");
|
|
inputs.push_back("input_1");
|
|
}
|
|
return inputs;
|
|
}
|
|
|
|
static std::string inferOutput(const std::string& source, const std::string& input) {
|
|
if (source.find("sort") != std::string::npos && input == "[3,1,2]") return "[1,2,3]";
|
|
if (source.find("sort") != std::string::npos && input == "[]") return "[]";
|
|
if (source.find("sort") != std::string::npos && input == "[1]") return "[1]";
|
|
if (source.find("sum") != std::string::npos && input == "[1,2,3]") return "6";
|
|
if (source.find("sum") != std::string::npos && input == "[]") return "0";
|
|
if (input.find("key=99") != std::string::npos) return "not_found";
|
|
if (input.find("key=2") != std::string::npos) return "found(2)";
|
|
return "expected_output";
|
|
}
|
|
|
|
static float computeConfidence(const std::string& sourceCode,
|
|
const std::string& targetCode,
|
|
const std::string& srcLang,
|
|
const std::string& tgtLang) {
|
|
// Direct stdlib mapping: high confidence
|
|
if (targetCode.find(".sort()") != std::string::npos ||
|
|
targetCode.find("sorted(") != std::string::npos ||
|
|
targetCode.find("Collections.sort") != std::string::npos)
|
|
return 0.95f;
|
|
// Idiomatic iterator patterns
|
|
if (targetCode.find(".iter()") != std::string::npos ||
|
|
targetCode.find(".stream()") != std::string::npos ||
|
|
targetCode.find("fold") != std::string::npos)
|
|
return 0.90f;
|
|
// Structural translation
|
|
if (targetCode.find("TODO") != std::string::npos ||
|
|
targetCode.find("STUB") != std::string::npos)
|
|
return 0.50f;
|
|
// Same language family
|
|
if (srcLang == tgtLang) return 0.95f;
|
|
return 0.75f;
|
|
}
|
|
};
|