2021-09-04 08:06:49 +00:00
|
|
|
/*
|
|
|
|
* Copyright (c) 2021 Huawei Device Co., Ltd.
|
|
|
|
* Licensed under the Apache License, Version 2.0 (the "License");
|
|
|
|
* you may not use this file except in compliance with the License.
|
|
|
|
* You may obtain a copy of the License at
|
|
|
|
*
|
|
|
|
* http://www.apache.org/licenses/LICENSE-2.0
|
|
|
|
*
|
|
|
|
* Unless required by applicable law or agreed to in writing, software
|
|
|
|
* distributed under the License is distributed on an "AS IS" BASIS,
|
|
|
|
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
|
|
* See the License for the specific language governing permissions and
|
|
|
|
* limitations under the License.
|
|
|
|
*/
|
|
|
|
|
|
|
|
#include "ecmascript/compiler/verifier.h"
|
|
|
|
|
2021-09-11 03:05:55 +00:00
|
|
|
#include <cmath>
|
2021-09-04 08:06:49 +00:00
|
|
|
#include <unordered_set>
|
|
|
|
|
|
|
|
#include "ecmascript/compiler/scheduler.h"
|
|
|
|
|
2021-12-23 06:55:22 +00:00
|
|
|
namespace panda::ecmascript::kungfu {
|
2021-09-04 08:06:49 +00:00
|
|
|
bool Verifier::RunDataIntegrityCheck(const Circuit *circuit)
|
|
|
|
{
|
2021-12-17 09:18:10 +00:00
|
|
|
std::unordered_set<GateRef> gatesSet;
|
|
|
|
std::vector<GateRef> gatesList;
|
2021-09-04 08:06:49 +00:00
|
|
|
gatesList.push_back(0);
|
|
|
|
gatesSet.insert(0);
|
|
|
|
size_t out = sizeof(Gate);
|
2021-12-17 09:18:10 +00:00
|
|
|
GateRef prevGate = 0;
|
2021-09-04 08:06:49 +00:00
|
|
|
while (true) {
|
2021-12-17 09:18:10 +00:00
|
|
|
GateRef gate = circuit->SaveGatePtr(
|
2021-09-04 08:06:49 +00:00
|
|
|
// NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic)
|
2021-12-17 09:18:10 +00:00
|
|
|
reinterpret_cast<const Out *>(circuit->LoadGatePtrConst(GateRef(out)))->GetGateConst());
|
2021-09-04 08:06:49 +00:00
|
|
|
if (gate < prevGate + static_cast<int64_t>(sizeof(Gate)) ||
|
|
|
|
gate >= static_cast<int64_t>(circuit->GetCircuitDataSize())) {
|
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (bad next gate)" << std::endl;
|
|
|
|
std::cerr << "at: " << std::dec << gate << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
gatesList.push_back(gate);
|
|
|
|
gatesSet.insert(gate);
|
|
|
|
prevGate = gate;
|
|
|
|
out += Gate::GetGateSize(
|
|
|
|
// NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic)
|
2021-12-17 09:18:10 +00:00
|
|
|
reinterpret_cast<const Out *>(circuit->LoadGatePtrConst(GateRef(out)))->GetIndex() + 1);
|
2021-09-04 08:06:49 +00:00
|
|
|
if (out == circuit->GetCircuitDataSize()) {
|
|
|
|
break;
|
|
|
|
}
|
|
|
|
if (out > circuit->GetCircuitDataSize() || out < 0) {
|
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (out of bound access)" << std::endl;
|
|
|
|
std::cerr << "at: " << std::dec << out << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
for (const auto &gate : gatesList) {
|
|
|
|
for (size_t idx = 0; idx < circuit->LoadGatePtrConst(gate)->GetNumIns(); idx++) {
|
|
|
|
const In *curIn = circuit->LoadGatePtrConst(gate)->GetInConst(idx);
|
|
|
|
if (!(circuit->GetSpaceDataStartPtrConst() < curIn && curIn < circuit->GetSpaceDataEndPtrConst())) {
|
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (corrupted in list)" << std::endl;
|
|
|
|
std::cerr << "id: " << std::dec << circuit->GetId(gate) << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (gatesSet.count(circuit->SaveGatePtr(curIn->GetGateConst())) == 0) {
|
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (invalid in address)" << std::endl;
|
|
|
|
std::cerr << "id: " << std::dec << circuit->GetId(gate) << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
{
|
|
|
|
const Gate *curGate = circuit->LoadGatePtrConst(gate);
|
|
|
|
if (!curGate->IsFirstOutNull()) {
|
|
|
|
const Out *curOut = curGate->GetFirstOutConst();
|
|
|
|
if (!(circuit->GetSpaceDataStartPtrConst() < curOut && curOut < circuit->GetSpaceDataEndPtrConst())) {
|
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (corrupted out list)" << std::endl;
|
|
|
|
std::cerr << "id: " << std::dec << circuit->GetId(gate) << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (gatesSet.count(circuit->SaveGatePtr(curOut->GetGateConst())) == 0) {
|
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (invalid out address)" << std::endl;
|
|
|
|
std::cerr << "id: " << std::dec << circuit->GetId(gate) << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
while (!curOut->IsNextOutNull()) {
|
|
|
|
curOut = curOut->GetNextOutConst();
|
|
|
|
if (!(circuit->GetSpaceDataStartPtrConst() < curOut &&
|
2021-09-07 14:24:16 +00:00
|
|
|
curOut < circuit->GetSpaceDataEndPtrConst())) {
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (corrupted out list)" << std::endl;
|
|
|
|
std::cerr << "id: " << std::dec << circuit->GetId(gate) << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (gatesSet.count(circuit->SaveGatePtr(curOut->GetGateConst())) == 0) {
|
|
|
|
std::cerr << "[Verifier][Error] Circuit data is corrupted (invalid out address)" << std::endl;
|
|
|
|
std::cerr << "id: " << std::dec << circuit->GetId(gate) << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Circuit data integrity is verified" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunStateGatesCheck(const Circuit *circuit, const std::vector<GateRef> &bbGatesList)
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
for (const auto &bbGate : bbGatesList) {
|
|
|
|
if (!circuit->Verify(bbGate)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] State gates input list schema is verified" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunCFGSoundnessCheck(const Circuit *circuit, const std::vector<GateRef> &bbGatesList,
|
|
|
|
const std::unordered_map<GateRef, size_t> &bbGatesAddrToIdx)
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
for (const auto &bbGate : bbGatesList) {
|
|
|
|
for (const auto &predGate : circuit->GetInVector(bbGate)) {
|
|
|
|
if (circuit->GetOpCode(predGate).IsState()) {
|
|
|
|
if (bbGatesAddrToIdx.count(predGate) == 0) {
|
|
|
|
std::cerr << "[Verifier][Error] CFG is not sound" << std::endl;
|
|
|
|
std::cerr << "Proof:" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(predGate) << ") is pred of "
|
|
|
|
<< "(id=" << circuit->GetId(bbGate) << ")" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(bbGate) << ") is reachable from entry" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(predGate) << ") is unreachable from entry" << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] CFG is sound" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
|
|
|
bool Verifier::RunCFGIsDAGCheck(const Circuit *circuit)
|
|
|
|
{
|
|
|
|
circuit->AdvanceTime();
|
2021-12-17 09:18:10 +00:00
|
|
|
std::function<bool(GateRef)> dfs = [&](GateRef cur) -> bool {
|
2021-09-04 08:06:49 +00:00
|
|
|
if (circuit->GetOpCode(cur) == OpCode::LOOP_BACK) {
|
|
|
|
return true;
|
|
|
|
}
|
|
|
|
circuit->SetMark(cur, MarkCode::VISITED);
|
|
|
|
for (const auto &succ : circuit->GetOutVector(cur)) {
|
|
|
|
if (circuit->GetOpCode(succ).IsState()) {
|
|
|
|
if (circuit->GetMark(succ) == MarkCode::VISITED) {
|
|
|
|
std::cerr << "[Verifier][Error] CFG without loop back edges is not directed acyclic graph"
|
|
|
|
<< std::endl;
|
|
|
|
std::cerr << "Proof:" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(succ) << ") is succ of "
|
|
|
|
<< "(id=" << circuit->GetId(cur) << ")" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(cur) << ") is reachable from "
|
|
|
|
<< "(id=" << circuit->GetId(succ) << ") without loop back edges" << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (circuit->GetMark(succ) == MarkCode::FINISHED) {
|
|
|
|
return true;
|
|
|
|
}
|
|
|
|
if (!dfs(succ)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
circuit->SetMark(cur, MarkCode::FINISHED);
|
|
|
|
return true;
|
|
|
|
};
|
|
|
|
auto root = Circuit::GetCircuitRoot(OpCode(OpCode::STATE_ENTRY));
|
|
|
|
if (!dfs(root)) {
|
|
|
|
return false;
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] CFG without loop back edges is directed acyclic graph" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunCFGReducibilityCheck(const Circuit *circuit, const std::vector<GateRef> &bbGatesList,
|
|
|
|
const std::unordered_map<GateRef, size_t> &bbGatesAddrToIdx,
|
2021-09-04 08:06:49 +00:00
|
|
|
const std::function<bool(size_t, size_t)> &isAncestor)
|
|
|
|
{
|
|
|
|
for (const auto &curGate : bbGatesList) {
|
|
|
|
if (circuit->GetOpCode(curGate) == OpCode::LOOP_BACK) {
|
|
|
|
for (const auto &succGate : circuit->GetOutVector(curGate)) {
|
|
|
|
if (circuit->GetOpCode(succGate).IsState()) {
|
|
|
|
bool isDom = isAncestor(bbGatesAddrToIdx.at(succGate), bbGatesAddrToIdx.at(curGate));
|
|
|
|
if (!isDom) {
|
|
|
|
std::cerr << "[Verifier][Error] CFG is not reducible" << std::endl;
|
|
|
|
std::cerr << "Proof:" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(succGate) << ") is loop back succ of "
|
|
|
|
<< "(id=" << circuit->GetId(curGate) << ")" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(succGate) << ") does not dominate "
|
|
|
|
<< "(id=" << circuit->GetId(curGate) << ")" << std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] CFG is reducible" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunFixedGatesCheck(const Circuit *circuit, const std::vector<GateRef> &fixedGatesList)
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
for (const auto &fixedGate : fixedGatesList) {
|
|
|
|
if (!circuit->Verify(fixedGate)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Fixed gates input list schema is verified" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunFixedGatesRelationsCheck(const Circuit *circuit, const std::vector<GateRef> &fixedGatesList,
|
|
|
|
const std::unordered_map<GateRef, size_t> &bbGatesAddrToIdx,
|
2021-09-04 08:06:49 +00:00
|
|
|
const std::function<bool(size_t, size_t)> &isAncestor)
|
|
|
|
{
|
|
|
|
for (const auto &fixedGate : fixedGatesList) {
|
|
|
|
size_t cnt = 0;
|
|
|
|
for (const auto &predGate : circuit->GetInVector(fixedGate)) {
|
|
|
|
if (circuit->GetOpCode(predGate).IsFixed() &&
|
|
|
|
circuit->GetOpCode(circuit->GetIn(predGate, 0)) != OpCode::LOOP_BACK) {
|
|
|
|
ASSERT(cnt > 0);
|
|
|
|
auto a = bbGatesAddrToIdx.at(circuit->GetIn(predGate, 0));
|
|
|
|
auto b = bbGatesAddrToIdx.at(circuit->GetIn(circuit->GetIn(fixedGate, 0), cnt - 1));
|
|
|
|
if (!isAncestor(a, b)) {
|
|
|
|
std::cerr << "[Verifier][Error] Fixed gates relationship is not consistent" << std::endl;
|
|
|
|
std::cerr << "Proof:" << std::endl;
|
|
|
|
std::cerr << "Fixed gate (id=" << predGate << ") is pred of fixed gate (id=" << fixedGate << ")"
|
|
|
|
<< std::endl;
|
|
|
|
std::cerr << "BB_" << bbGatesAddrToIdx.at(circuit->GetIn(predGate, 0)) << " does not dominate BB_"
|
|
|
|
<< bbGatesAddrToIdx.at(circuit->GetIn(circuit->GetIn(fixedGate, 0), cnt - 1))
|
|
|
|
<< std::endl;
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
cnt++;
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Fixed gates relationship is consistent" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunFlowCyclesFind(const Circuit *circuit, std::vector<GateRef> *schedulableGatesListPtr,
|
|
|
|
const std::vector<GateRef> &bbGatesList, const std::vector<GateRef> &fixedGatesList)
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
circuit->AdvanceTime();
|
2021-12-17 09:18:10 +00:00
|
|
|
std::vector<GateRef> startGateList;
|
2021-09-04 08:06:49 +00:00
|
|
|
for (const auto &gate : bbGatesList) {
|
|
|
|
for (const auto &predGate : circuit->GetInVector(gate)) {
|
|
|
|
if (circuit->GetOpCode(predGate).IsSchedulable()) {
|
|
|
|
if (circuit->GetMark(predGate) == MarkCode::EMPTY) {
|
|
|
|
startGateList.push_back(predGate);
|
|
|
|
circuit->SetMark(predGate, MarkCode::VISITED);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
for (const auto &gate : fixedGatesList) {
|
|
|
|
for (const auto &predGate : circuit->GetInVector(gate)) {
|
|
|
|
if (circuit->GetOpCode(predGate).IsSchedulable()) {
|
|
|
|
if (circuit->GetMark(predGate) == MarkCode::EMPTY) {
|
|
|
|
startGateList.push_back(predGate);
|
|
|
|
circuit->SetMark(predGate, MarkCode::VISITED);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
circuit->AdvanceTime();
|
2021-12-17 09:18:10 +00:00
|
|
|
std::vector<GateRef> cycleGatesList;
|
|
|
|
GateRef meet = -1;
|
|
|
|
std::function<bool(GateRef)> dfs = [&](GateRef cur) -> bool {
|
2021-09-04 08:06:49 +00:00
|
|
|
circuit->SetMark(cur, MarkCode::VISITED);
|
|
|
|
schedulableGatesListPtr->push_back(cur);
|
|
|
|
size_t numIns = circuit->LoadGatePtrConst(cur)->GetNumIns();
|
|
|
|
for (size_t idx = 0; idx < numIns; idx++) {
|
|
|
|
const auto prev = circuit->GetIn(cur, idx);
|
|
|
|
if (circuit->GetOpCode(prev).IsSchedulable()) {
|
|
|
|
if (circuit->GetMark(prev) == MarkCode::VISITED) {
|
|
|
|
std::cerr << "[Verifier][Error] Found a data or depend flow cycle without passing selectors"
|
|
|
|
<< std::endl;
|
|
|
|
std::cerr << "Proof:" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(prev) << ") is prev of "
|
|
|
|
<< "(id=" << circuit->GetId(cur) << ")" << std::endl;
|
|
|
|
std::cerr << "(id=" << circuit->GetId(prev) << ") is reachable from "
|
|
|
|
<< "(id=" << circuit->GetId(cur) << ") without passing selectors" << std::endl;
|
|
|
|
meet = prev;
|
|
|
|
cycleGatesList.push_back(cur);
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (circuit->GetMark(prev) != MarkCode::FINISHED) {
|
|
|
|
if (!dfs(prev)) {
|
|
|
|
if (meet != -1) {
|
|
|
|
cycleGatesList.push_back(cur);
|
|
|
|
}
|
|
|
|
if (meet == cur) {
|
|
|
|
meet = -1;
|
|
|
|
}
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
circuit->SetMark(cur, MarkCode::FINISHED);
|
|
|
|
return true;
|
|
|
|
};
|
|
|
|
for (const auto &startGate : startGateList) {
|
|
|
|
if (circuit->GetMark(startGate) == MarkCode::EMPTY) {
|
|
|
|
if (!dfs(startGate)) {
|
|
|
|
std::cerr << "Path:" << std::endl;
|
|
|
|
for (const auto &cycleGate : cycleGatesList) {
|
|
|
|
circuit->Print(cycleGate);
|
|
|
|
}
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Every directed data or depend flow cycles in circuit contain selectors" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunSchedulableGatesCheck(const Circuit *circuit, const std::vector<GateRef> &schedulableGatesList)
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
for (const auto &schedulableGate : schedulableGatesList) {
|
|
|
|
if (!circuit->Verify(schedulableGate)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Schedulable gates input list schema is verified" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunPrologGatesCheck(const Circuit *circuit, const std::vector<GateRef> &schedulableGatesList)
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
for (const auto &schedulableGate : schedulableGatesList) {
|
|
|
|
for (const auto &predGate : circuit->GetInVector(schedulableGate)) {
|
|
|
|
if (circuit->GetOpCode(predGate).IsProlog()) {
|
|
|
|
if (!circuit->Verify(predGate)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Prolog gates input list schema is verified" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
bool Verifier::RunSchedulingBoundsCheck(const Circuit *circuit, const std::vector<GateRef> &schedulableGatesList,
|
|
|
|
const std::unordered_map<GateRef, size_t> &bbGatesAddrToIdx,
|
2021-09-04 08:06:49 +00:00
|
|
|
const std::function<bool(size_t, size_t)> &isAncestor,
|
|
|
|
const std::function<size_t(size_t, size_t)> &lowestCommonAncestor)
|
|
|
|
{
|
|
|
|
// check existence of scheduling upper bound
|
2021-12-17 09:18:10 +00:00
|
|
|
std::unordered_map<GateRef, size_t> upperBound;
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
auto result =
|
|
|
|
Scheduler::CalculateSchedulingUpperBound(circuit, bbGatesAddrToIdx, isAncestor, schedulableGatesList);
|
|
|
|
if (!result.has_value()) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
upperBound = result.value();
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Scheduling upper bounds of all schedulable gates exist" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
}
|
|
|
|
// check existence of scheduling lower bound
|
2021-12-17 09:18:10 +00:00
|
|
|
std::unordered_map<GateRef, size_t> lowerBound;
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
|
|
|
auto result = Scheduler::CalculateSchedulingLowerBound(circuit, bbGatesAddrToIdx, lowestCommonAncestor);
|
|
|
|
lowerBound = result.value();
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Scheduling lower bounds of all schedulable gates exist" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
}
|
|
|
|
// check consistency of lower bound and upper bound
|
|
|
|
{
|
|
|
|
ASSERT(upperBound.size() == lowerBound.size());
|
|
|
|
for (const auto &item : lowerBound) {
|
|
|
|
if (!isAncestor(upperBound.at(item.first), lowerBound.at(item.first))) {
|
|
|
|
std::cerr << "[Verifier][Error] Bounds of gate (id=" << item.first << ") is not consistent"
|
|
|
|
<< std::endl;
|
|
|
|
std::cerr << "Proof:" << std::endl;
|
|
|
|
std::cerr << "Upper bound is BB_" << upperBound.at(item.first) << std::endl;
|
|
|
|
std::cerr << "Lower bound is BB_" << lowerBound.at(item.first) << std::endl;
|
|
|
|
}
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
#if ECMASCRIPT_ENABLE_COMPILER_LOG
|
2021-09-04 08:06:49 +00:00
|
|
|
std::cerr << "[Verifier][Pass] Bounds of all schedulable gates are consistent" << std::endl;
|
2021-12-17 09:18:10 +00:00
|
|
|
#endif
|
2021-09-04 08:06:49 +00:00
|
|
|
}
|
|
|
|
return true;
|
|
|
|
}
|
|
|
|
|
2021-12-17 09:18:10 +00:00
|
|
|
std::vector<GateRef> Verifier::FindFixedGates(const Circuit *circuit, const std::vector<GateRef> &bbGatesList)
|
2021-09-04 08:06:49 +00:00
|
|
|
{
|
2021-12-17 09:18:10 +00:00
|
|
|
std::vector<GateRef> fixedGatesList;
|
2021-09-04 08:06:49 +00:00
|
|
|
for (const auto &bbGate : bbGatesList) {
|
|
|
|
for (const auto &succGate : circuit->GetOutVector(bbGate)) {
|
|
|
|
if (circuit->GetOpCode(succGate).IsFixed()) {
|
|
|
|
fixedGatesList.push_back(succGate);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return fixedGatesList;
|
|
|
|
}
|
|
|
|
|
|
|
|
bool Verifier::Run(const Circuit *circuit)
|
|
|
|
{
|
|
|
|
if (!RunDataIntegrityCheck(circuit)) {
|
|
|
|
return false;
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
std::vector<GateRef> bbGatesList;
|
|
|
|
std::unordered_map<GateRef, size_t> bbGatesAddrToIdx;
|
2021-09-04 08:06:49 +00:00
|
|
|
std::vector<size_t> immDom;
|
|
|
|
std::tie(bbGatesList, bbGatesAddrToIdx, immDom) = Scheduler::CalculateDominatorTree(circuit);
|
|
|
|
std::cerr << std::dec;
|
|
|
|
if (!RunStateGatesCheck(circuit, bbGatesList)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (!RunCFGSoundnessCheck(circuit, bbGatesList, bbGatesAddrToIdx)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (!RunCFGIsDAGCheck(circuit)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
std::vector<std::vector<size_t>> sonList(bbGatesList.size());
|
|
|
|
for (size_t idx = 1; idx < immDom.size(); idx++) {
|
|
|
|
sonList[immDom[idx]].push_back(idx);
|
|
|
|
}
|
2021-09-07 14:24:16 +00:00
|
|
|
const size_t sizeLog = std::ceil(std::log2(static_cast<double>(bbGatesList.size())) + 1);
|
2021-09-04 08:06:49 +00:00
|
|
|
std::vector<size_t> timeIn(bbGatesList.size());
|
|
|
|
std::vector<size_t> timeOut(bbGatesList.size());
|
|
|
|
std::vector<std::vector<size_t>> jumpUp;
|
|
|
|
jumpUp.assign(bbGatesList.size(), std::vector<size_t>(sizeLog + 1));
|
|
|
|
{
|
|
|
|
size_t timestamp = 0;
|
|
|
|
std::function<void(size_t, size_t)> dfs = [&](size_t cur, size_t prev) {
|
|
|
|
timeIn[cur] = timestamp++;
|
|
|
|
jumpUp[cur][0] = prev;
|
|
|
|
for (size_t stepSize = 1; stepSize <= sizeLog; stepSize++) {
|
|
|
|
jumpUp[cur][stepSize] = jumpUp[jumpUp[cur][stepSize - 1]][stepSize - 1];
|
|
|
|
}
|
|
|
|
for (const auto &succ : sonList[cur]) {
|
|
|
|
dfs(succ, cur);
|
|
|
|
}
|
|
|
|
timeOut[cur] = timestamp++;
|
|
|
|
};
|
|
|
|
size_t root = 0;
|
|
|
|
dfs(root, root);
|
|
|
|
}
|
|
|
|
auto isAncestor = [timeIn, timeOut](size_t nodeA, size_t nodeB) -> bool {
|
|
|
|
return timeIn[nodeA] <= timeIn[nodeB] && timeOut[nodeA] >= timeOut[nodeB];
|
|
|
|
};
|
|
|
|
auto lowestCommonAncestor = [&](size_t nodeA, size_t nodeB) -> size_t {
|
|
|
|
if (isAncestor(nodeA, nodeB)) {
|
|
|
|
return nodeA;
|
|
|
|
}
|
|
|
|
if (isAncestor(nodeB, nodeA)) {
|
|
|
|
return nodeB;
|
|
|
|
}
|
|
|
|
for (size_t stepSize = sizeLog + 1; stepSize > 0; stepSize--) {
|
|
|
|
if (!isAncestor(jumpUp[nodeA][stepSize - 1], nodeB)) {
|
|
|
|
nodeA = jumpUp[nodeA][stepSize - 1];
|
|
|
|
}
|
|
|
|
}
|
|
|
|
return jumpUp[nodeA][0];
|
|
|
|
};
|
|
|
|
if (!RunCFGReducibilityCheck(circuit, bbGatesList, bbGatesAddrToIdx, isAncestor)) {
|
|
|
|
return false;
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
std::vector<GateRef> fixedGatesList = FindFixedGates(circuit, bbGatesList);
|
2021-09-04 08:06:49 +00:00
|
|
|
if (!RunFixedGatesCheck(circuit, fixedGatesList)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (!RunFixedGatesRelationsCheck(circuit, fixedGatesList, bbGatesAddrToIdx, isAncestor)) {
|
|
|
|
return false;
|
|
|
|
}
|
2021-12-17 09:18:10 +00:00
|
|
|
std::vector<GateRef> schedulableGatesList;
|
2021-09-04 08:06:49 +00:00
|
|
|
if (!RunFlowCyclesFind(circuit, &schedulableGatesList, bbGatesList, fixedGatesList)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (!RunSchedulableGatesCheck(circuit, fixedGatesList)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (!RunPrologGatesCheck(circuit, fixedGatesList)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
if (!RunSchedulingBoundsCheck(circuit, schedulableGatesList, bbGatesAddrToIdx, isAncestor, lowestCommonAncestor)) {
|
|
|
|
return false;
|
|
|
|
}
|
|
|
|
return true;
|
|
|
|
}
|
2021-12-23 06:55:22 +00:00
|
|
|
} // namespace panda::ecmascript::kungfu
|