Souper 분석 관련 키워드들

1. Cadidate

// breadth-first search
void souper::findCands(Inst *Root, std::set<Inst *> &Guesses,
		       bool WidthMustMatch, bool FilterVars,int Max) {
  std::set<Inst *> Visited;
  std::queue<Inst *> Q;
  Q.push(Root);
  while (!Q.empty()) {
    Inst *I = Q.front();
    Q.pop();
    if (Visited.insert(I).second) {
      for (auto Op : I->Ops)
        Q.push(Op);
      if (I->Available && I->K != Inst::Const
          && I->K != Inst::UntypedConst) {
        if (WidthMustMatch && I->Width != Root->Width)
          continue;
        if (FilterVars && I->K == Inst::Var)
          continue;
        if (I->K == Inst::SAddWithOverflow || I->K == Inst::UAddWithOverflow ||
            I->K == Inst::SSubWithOverflow || I->K == Inst::USubWithOverflow ||
            I->K == Inst::SMulWithOverflow || I->K == Inst::UMulWithOverflow ||
            I->K == Inst::SAddO || I->K == Inst::UAddO ||
            I->K == Inst::SSubO || I->K == Inst::USubO ||
            I->K == Inst::SMulO || I->K == Inst::UMulO)
          continue;
        if (Guesses.size() < Max)
          Guesses.insert(I);
      }
    }
  }
}

candidates : [ 0] 
%0:i32 = var ; 0
=================================
candidates : [ 1] 
%0:i32 = var ; 1
=================================
candidates : [ 2] 
%0:i32 = var ; 0
%1:i32 = var ; 1
%2:i32 = xor %0, %1
=================================
candidates : [ 3] 
%0:i32 = var ; 1
%1:i32 = var ; 0
%2:i32 = xor %1, %0
%3:i32 = xor %0, %2
=================================

 

 

2. infer 는 어디서 어떻게 추가 되는가?

 

             :========== Back-trace ==========
   38.708 us :   ~T~\ ~T~@(1) souper::PrintReplacementLHS
   38.708 us :   ~T~B (1) souper::GetReplacementLHSString::cxx11
   38.708 us :   ~T~B (1) _GLOBAL__N_1::MemCachingSolver::infer
   38.708 us :   ~T~B (1) SolveInst
   38.708 us :   ~T~B (1) main
             :   ~T~B
   42.250 us :   ~T~T ~T~@(1) souper::PrintReplacementLHS
   42.250 us :    (1) souper::GetReplacementLHSString::cxx11
   42.250 us :    (1) synthesizeWithKLEE
   42.250 us :    (1) souper::EnumerativeSynthesis::synthesize
   42.250 us :    (1) _GLOBAL__N_1::BaseSolver::inferHelper                                                                                                          
   42.250 us :    (1) _GLOBAL__N_1::BaseSolver::infer
   42.250 us :    (1) _GLOBAL__N_1::MemCachingSolver::infer
   42.250 us :    (1) SolveInst
   42.250 us :    (1) main

 

void souper::PrintReplacementLHS(llvm::raw_ostream &Out,
                                 const BlockPCs &BPCs,
                                 const std::vector<InstMapping> &PCs,
                                 Inst *LHS, ReplacementContext &Context,
                                 bool printNames) {
  assert(LHS);
  assert(Context.empty());

  Context.printPCs(PCs, Out, printNames);
  Context.printBlockPCs(BPCs, Out, printNames);
  std::string SRef = Context.printInst(LHS, Out, printNames);

  Out << "infer " << SRef;
  if (!LHS->DemandedBits.isAllOnesValue()) {
    Out<< " (" << "demandedBits="
       << Inst::getDemandedBitsString(LHS->DemandedBits)
       << ")";
  }
  if (LHS->HarvestKind == HarvestType::HarvestedFromUse) {
    Out << " (harvestedFromUse)";
  }
  Out << "\n";
}

--------------------- synthesizeWithKLEE ---------------------------
%0:i32 = var
%1:i32 = var
%2:i32 = xor %0, %1
%3:i32 = xor %1, %2
%4:i32 = xor %2, %3
infer %4

there are 5 guesses to check

--------------------------------

 

 

3. infer는 어떻게 역할하는가?

infer 는 키워드

 

 

4. synthesize 과정

 

:========== Back-trace ==========
  614.174 ms : (1) synthesizeWithKLEE
  614.174 ms : (1) souper::EnumerativeSynthesis::synthesize
  614.174 ms : (1) _GLOBAL__N_1::BaseSolver::inferHelper
  614.174 ms : (1) _GLOBAL__N_1::BaseSolver::infer
  614.174 ms : (1) _GLOBAL__N_1::MemCachingSolver::infer
  614.174 ms : (1) SolveInst
  614.174 ms : (1) main

 

  426.301 ms :   ~T~\ ~V (1) souper::ConstantSynthesis::synthesize
             :   ~T~B
  187.220 ms :   ~T~\ ~V (2) isConcreteCandidateSat

 

 

5. CEGIS (counterexample guided inductive synthesis )

 

Counterexample-Guided Inductive Synthesis (CEGIS)는 프로그램이나 회로 디자인과 같은 자동 합성 문제를 해결하기 위한 컴퓨터 과학 기술 중 하나입니다. CEGIS는 주어진 명세를 만족하는 프로그램 또는 회로를 찾는 과정에서 반복적으로 예외 상황 (카운터 예제)을 사용하여 합성을 안내합니다.

CEGIS는 다음과 같은 주요 단계로 이루어집니다:

1. 명세 정의: 먼저 원하는 동작을 명세화합니다. 이 명세는 입력과 출력 사이의 관계를 정의하거나, 원하는 속성 및 제약 조건을 포함할 수 있습니다.
2. 프로그램 형태 선정: 합성될 프로그램 또는 회로의 형태를 선택합니다. 이 형태는 기본적인 구조와 변수, 연산 등을 포함할 것입니다.
3. 초기 후보 생성: 합성 프로세스를 시작하면 초기 후보 프로그램 또는 회로를 생성합니다. 이 후보는 보통 무작위로 생성되거나, 기본 구조에 따라 생성됩니다.
4. 검증 단계: 초기 후보를 사용하여 명세를 만족하는지 확인합니다. 즉, 합성된 프로그램이 주어진 명세를 따르는지 여부를 검사합니다. 만약 만족하지 않으면, 카운터 예제를 찾습니다.
5. 카운터 예제 발견: 검증 과정에서 만족하지 않는 부분을 찾으면, 이를 카운터 예제로 사용합니다. 이 예제는 명세를 위반하는 입력 또는 상황을 나타냅니다.
6. 합성 업데이트: 카운터 예제를 사용하여 초기 후보를 개선하거나 새로운 후보를 생성합니다. 이때 카운터 예제에 대한 수정을 통해 명세를 만족하는 프로그램을 더 잘 맞출 수 있도록 합니다.
7. 반복: 검증 및 업데이트 단계를 반복합니다. 합성 프로세스는 카운터 예제를 찾을 때까지 또는 주어진 시간 또는 리소스 한도 내에서 계속됩니다.
8. 성공 또는 실패: 만약 명세를 만족하는 프로그램이 발견되면 성공으로 간주하고, 그렇지 않으면 실패로 간주합니다.

CEGIS는 자동 프로그램 합성, 회로 설계, 소프트웨어 검증 및 다른 영역에서 활발하게 사용되는 기술입니다. 주요 장점 중 하나는 사용자가 명세만 정의하고 합성 프로세스가 나머지 작업을 처리한다는 것입니다. 그러나 CEGIS가 효과적으로 작동하려면 검증 과정이 비교적 효율적이어야 하며, 검증 과정의 결과로 카운터 예제를 얻을 수 있어야 합니다.

 

 

 

 

$\exists \mathbf{P} \cdot Q \mathbf{x} \cdot \sigma(\mathbf{P}, \mathbf{x})$

 

주어진 수식 "∃P⋅Qx⋅σ(P, x)"는 일반적으로 논리식에서 사용되며, 양자화자(existential quantifier)와 함수 또는 술어(predicate)로 이루어진 구조를 나타냅니다. 이 수식을 다음과 같이 해석할 수 있습니다:

• "∃P": 이 부분은 양자화자(existential quantifier)로, "존재한다" 또는 "어떤 것이 있다"를 나타냅니다. P는 어떤 변수나 변수 집합을 나타내며, 이 변수들이 어떤 조건을 충족하는 경우를 나타냅니다.
• "Qx": 이 부분은 변수 x에 어떤 조건 Q가 적용됨을 나타냅니다. 즉, x가 어떤 조건 Q를 만족하는 경우를 나타냅니다.
• "σ(P, x)": σ(P, x)는 함수 또는 술어(predicate)로, 변수 P와 x에 의존하는 것을 나타냅니다. 이 부분은 주어진 변수 P와 x에 대한 조건 또는 관계를 나타내며, P와 x가 주어진 조건을 만족하는 경우를 나타냅니다.

따라서 전체 수식 "∃P⋅Qx⋅σ(P, x)"는 어떤 변수 P와 변수 x에 대한 조건이 주어지고, 그 조건을 만족하는 경우가 적어도 하나 존재한다는 것을 나타냅니다. 이 수식은 논리적으로 P와 x에 대한 관계를 나타내고, P와 x가 주어진 조건을 만족하는 경우가 하나 이상 있다는 것을 나타냅니다. 이것은 일반적으로 논리적 추론 및 논리적 증명에서 사용됩니다