Speculation -spec-type=safety not working on one example.

[rasoolmaghareh]

In the master branch, speculation with -spec-type=safety and all the three strategies (timid, aggressive and custom) is not working on this example. However, when I run this program on the speculation branch speculation is performed successfully:

#include <klee/klee.h>

int main() {

    char b0,b1,b2;

    int x = 0;
    int y = 0,z=0, w=1;

    klee_make_symbolic(&b0, sizeof(char), "b0");
    klee_make_symbolic(&b1, sizeof(char), "b1");
    klee_make_symbolic(&b2, sizeof(char), "b2");

    if (b1 > 0) x = x + 3; else x = x + 0;
    if (b2 > 0) x = x + 6; else x = x + 0;
    if (b3 > 0) x = x + 9; else x = x + 0;
    int BOUND = 7;
    if (BOUND == x) {y++; z = z + 2; } else y--;
    if (x % 2 ==0 ) {w = w + 3; } else w = w + z;
    klee_assert( 2*y <= z && 3*y <= w);
    return 0;
}

For example, on the following attached c code, the speculation finishes quite fast:

KLEE: done: total instructions = 1880
KLEE: done: completed paths = 200, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 100
KLEE: done:     average branching depth of subsumed paths = 50.5
KLEE: done:     average instructions of completed paths = 931
KLEE: done:     average instructions of subsumed paths = 562.01
KLEE: done:     subsumed paths = 196
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 4
KLEE: done: generated tests = 3, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 3

While for the master branch after 30 seconds, I stopped the analysis with the following results:

KLEE: done: total instructions = 178201
KLEE: done: completed paths = 10814, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 90
KLEE: done:     average branching depth of completed paths = 96.0978
KLEE: done:     average branching depth of subsumed paths = 94.8565
KLEE: done:     average instructions of completed paths = 925.52
KLEE: done:     average instructions of subsumed paths = 879.476
KLEE: done:     subsumed paths = 8350
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 2374
KLEE: done: generated tests = 99, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 78
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 21

spec.c.zip

[rasoolmaghareh]

Also @sanghu1790 has reported that the following program is slow on speculation with -spec-strategy=custom -spec-type=safety.

#include<stdio.h>
#ifdef LLBMC
#include <llbmc.h>
#else
#include <klee/klee.h>
#endif
typedef int bool;
int kappa  =    0;
char r1  ;
bool mode1  ;
bool mode2  ;
bool mode3  ;
void node1(void) 
{ 

  {
  if (mode1) {
    if ((int )r1 == 255) {
    kappa++;
      r1 = (char)2;

    }
    r1 = (char )((int )r1 + 1);
    mode1 = 0;
  }
  return;
}
}

void node2(void) 
{ 

  {
  if (mode2) {
    if ((int )r1 == 255) {
      r1 = (char)2;
    }
    r1 = (char )((int )r1 + 1);
    mode2 = 0;

  }
  return;
}
}

void node3(void) 
{ 
  {
  if (mode3) {

    if ((int )r1 == 255) {
      r1 = (char)2;
    }
    r1 = (char )((int )r1 + 1);
    mode3 = 0;
  }
  return;
}
}

int main(void) 
{ int i2 ;

  {
  klee_make_symbolic(& r1, sizeof(char ), "r1");
  klee_make_symbolic(& mode1, sizeof(bool ), "mode1");
  klee_make_symbolic(& mode2, sizeof(bool ), "mode2");
  klee_make_symbolic(& mode3, sizeof(bool ), "mode3");
  i2 = 0;
  while (i2 < 2) {
    node1();
    node2();
    node3();
    i2 = i2 + 1;
  }
  klee_assert(kappa < 1);
  //_SLICE(kappa);
  return (0);
}
}

[xuanlinhha]

@rasoolmaghareh on which branch of speculation do you run? spec_aggressive spec_custom spec_custom_dyn spec_timid

[rasoolmaghareh]

The Speculation branch:

https://github.com/tracer-x/klee/tree/Speculation

[xuanlinhha]

But we didn't work on that branch @rasoolmaghareh I remember we work and merge from branch beginning with spec_

[rasoolmaghareh]

@linh, I mean the old speculation branch. Can you please post the results of your comparison with master branch here?

[xuanlinhha]

sp-bug3.c.txt info-master.txt info-Speculation.txt

I see their running times are not much different on my machine

[rasoolmaghareh]

sp-bug3.c.txt info-master.txt info-Speculation.txt

I see their running times are not much different on my machine

@xuanlinhha, I noticed you have not added the -speculation while running on the speculation branch. After adding the speculation branch the results are much different:

KLEE: done: total instructions = 1096
KLEE: done: completed paths = 102, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 51
KLEE: done:     average branching depth of subsumed paths = 26
KLEE: done:     average instructions of completed paths = 588
KLEE: done:     average instructions of subsumed paths = 390.52
KLEE: done:     subsumed paths = 98
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 4
KLEE: done: generated tests = 3, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 3

[rasoolmaghareh]

Summary of today's discussion:

The issue in the slowness (loss of subsumptions) of -spec-type=safety speculation is the dependence check and also the check for new basic blocks:

  llvm::BasicBlock *currentBB = current.txTreeNode->getBasicBlock();
  if (visitedBlocks.find(currentBB) == visitedBlocks.end()) {
    specFail++;
    speculativeBackJump(current, true);
    return StatePair(0, 0);
  }

These checks are not required for safety but are required for coverage.

The suggestion is as follows:

1- creating a new branch speculation_safety_fix 2- for the -spec-type=safety option, we turn off these two checks.

[rasoolmaghareh]

@xuanlinhha: I have checked the speculation_safety_fix branch and it is showing correct results on our test program, please proceed to to generate a branch on master to apply these two changes for -spec-type=safety

[rasoolmaghareh]

Hi Linh,

I have checked the code. Speculation -spec-type=safety and -spec-strategy=aggressive is working fine. However, -spec-strategy=timid and -spec-strategy=custom are not working fine.

The question I am trying to answer is that if we turn off the dependence check and also new basic-block check, then what is the difference between aggressive and, timid and custom?

Can you tell me what is the difference between these three strategies when running with -spec-type=safety?

I am thinking about dropping strategy when doing -spec-type=safety. May I know what you think @xuanlinhha @sanghu1790?

Results for -spec-type=safety and aggressive:

KLEE: done: total instructions = 1096
KLEE: done: completed paths = 102, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 51
KLEE: done:     average branching depth of subsumed paths = 26
KLEE: done:     average instructions of completed paths = 588
KLEE: done:     average instructions of subsumed paths = 390.52
KLEE: done:     subsumed paths = 98
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 4
KLEE: done: generated tests = 3, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 3

Results for -spec-type=safety and timid:

KLEE: done: total instructions = 406495
KLEE: done: completed paths = 39016, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 49
KLEE: done:     average branching depth of subsumed paths = 37.5849
KLEE: done:     average instructions of completed paths = 604.946
KLEE: done:     average instructions of subsumed paths = 484.066
KLEE: done:     subsumed paths = 36570
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 2446
KLEE: done: generated tests = 51, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 51

Results for -spec-type=safety and custom:

KLEE: done: total instructions = 406495
KLEE: done: completed paths = 39016, among which
KLEE: done:     early-terminating paths (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     average branching depth of completed paths = 49
KLEE: done:     average branching depth of subsumed paths = 37.5849
KLEE: done:     average instructions of completed paths = 604.946
KLEE: done:     average instructions of subsumed paths = 484.066
KLEE: done:     subsumed paths = 36570
KLEE: done:     error paths = 0
KLEE: done:     program exit paths = 2446
KLEE: done: generated tests = 51, among which
KLEE: done:     early-terminating tests (instruction time limit, solver timeout, max-depth reached) = 0
KLEE: done:     error tests = 0
KLEE: done:     program exit tests = 51

[xuanlinhha]

If -spec-type=safety, I turned off 2 checkings for all strategies

if (SpecTypeToUse == SAFETY) {
        if (SpecStrategyToUse == TIMID) {
          StatsTracker::increaseEle(curBB, 1, true);
        } else if (SpecStrategyToUse == AGGRESSIVE) {
          // open speculation & result may be success or fail
          StatsTracker::increaseEle(curBB, 0, true);
          return addSpeculationNode(current, condition, binst, isInternal,
                                    true);
        } else if (SpecStrategyToUse == CUSTOM) {
          // open speculation & result may be success or fail and Now second
          // check
          if (specSnap[binst] != visitedBlocks.size()) {
            dynamicYes++;
            StatsTracker::increaseEle(curBB, 0, true);
            return addSpeculationNode(current, condition, binst, isInternal,
                                      true);
          } else {
            dynamicNo++;
            // then close speculation & do marking as deletion
            txTree->markPathCondition(current, unsatCore);
            return StatePair(&current, 0);
          }
        }
      } else {
        if (SpecStrategyToUse == TIMID) {
          std::set<std::string> vars = extractVarNames(current, binst);
          if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
            independenceYes++;
            StatsTracker::increaseEle(curBB, 0, true);
            StatsTracker::increaseEle(curBB, 2, false);
          } else {
            independenceNo++;
            StatsTracker::increaseEle(curBB, 1, true);
          }
        } else if (SpecStrategyToUse == AGGRESSIVE) {
          // check independency
          std::set<std::string> vars = extractVarNames(current, binst);
          if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
            // open speculation & assume success
            independenceYes++;
            StatsTracker::increaseEle(curBB, 0, true);
            StatsTracker::increaseEle(curBB, 2, false);
            return StatePair(&current, 0);
          } else {
            // open speculation & result may be success or fail
            independenceNo++;
            StatsTracker::increaseEle(curBB, 0, true);
            return addSpeculationNode(current, condition, binst, isInternal,
                                      true);
          }
        } else if (SpecStrategyToUse == CUSTOM) {
          // check independency
          std::set<std::string> vars = extractVarNames(current, binst);
          if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
            // open speculation & assume success
            independenceYes++;
            //          StatsTracker::increaseEle(curBB, 0, true);
            //          StatsTracker::increaseEle(curBB, 2, false);
            return StatePair(&current, 0);
          } else {
            // open speculation & result may be success or fail and Now second
            // check
            independenceNo++;
            if (specSnap[binst] != visitedBlocks.size()) {
              dynamicYes++;
              StatsTracker::increaseEle(curBB, 0, true);
              return addSpeculationNode(current, condition, binst, isInternal,
                                        true);
            } else {
              dynamicNo++;
              // then close speculation & do marking as deletion
              txTree->markPathCondition(current, unsatCore);
              return StatePair(&current, 0);
            }
          }
        }
      }

[sanghu1790]

@rasoolmaghareh I feel, type safety and coverage both are important for all versions timid, aggressive, and custom. Timid is more light weight and aggressive is more heavy weight. However, custom_dyn is reasonable because of choice of speculation. As you said, for safety "new basic-block check" is disabled for all three version which is correct. But, when we say "dependence check" turned off, it means we dont check the independence checks of Spec_Avoid files(if supplied which I expect is required) within "speculationFork" however independence checks will be there in "branchFork". I suspect the the statistics you are getting different because of this incompatibility. @xuanlinhha May I request you to check in this fix branch for timid, aggressive, and custom, where,

1. We all time do independence check in branchFork and speculationFork? YES/NO
2. We do independence check in branchFork and not speculationFork for all three? YES/NO
3. We do independence check in branchFork and not speculationFork for timid and custom? YES/NO
4. We do independence check in branchFork and speculationFork for aggressive, and not for others?YES/NO

@rasoolmaghareh Rasool I feel before dropping the strategy and taking the decision lets get above answers from @xuanlinhha. I remember, we took decision regarding the checks on/off of on branches, that's why statistics are different.

[rasoolmaghareh]

sure, let's wait for Linh's response.

[xuanlinhha]

Based on the last commit of this branch: maste_speculation_safety_fix

1. NO Because if type is safety we do not check independency in branchFork
2. NO Because we check independency for CUSTOM in speculationFork
3. NO Because in branchFork we do not check independency if type is safety
4. NO Because in branchFork, if type is safety, we also do not check independency for aggressive

[sanghu1790]

@xuanlinhha Thanks for answers. In conclusion, we dont do "independency check" in branchFork for all three timid, aggressive, and custom. We do "independency check" in speculationFork for CUSTOM only and not for timid and aggressive. I think something is wrong as per our original definitions we decided. My interpretation: I always believed that for safety and coverage strategies we always do independence checks in branchFork, and I remember we had some choice to turn on/off the checks in speculationFork in all the three versions. I am pretty sure that the difference we decided in between safety and coverage strategies was just only disabling the "new basic-block check" in safety thats all, and other features will be as it is same. But, here the scenario is very different. What I can see is that for timid and aggressive there is no need to supply Spec_Avoid files entirely if safety is enabled, which we never decided to do. That's why all time I was saying that we need to supply Spec_Avoid files to all versions on both safety and coverage strategies. In performance, I remember safety would be little faster but may not give accurate block coverage, but for coverage strategy performance will be little slower and block coverage will be accurate (since if coverage enabled it does both safety and coverage).

@rasoolmaghareh Do you remember anything if we took such above decision? Can you see a lot of ambiguities? @rasoolmaghareh and @xuanlinhha I think we need to discuss on this. Thanks, Sanghu

[xuanlinhha]

This is in branchFork

if (INTERPOLATION_ENABLED && SpecTypeToUse != NO_SPEC &&
        TxSpeculationHelper::isStateSpeculable(current)) {
  ...
  if (SpecTypeToUse == SAFETY) {
    if (SpecStrategyToUse == TIMID) {
      StatsTracker::increaseEle(curBB, 1, true);
    } else if (SpecStrategyToUse == AGGRESSIVE) {
      // open speculation & result may be success or fail
      StatsTracker::increaseEle(curBB, 0, true);
      return addSpeculationNode(current, condition, binst, isInternal,
                                true);
    } else if (SpecStrategyToUse == CUSTOM) {
      // open speculation & result may be success or fail and Now second
      // check
      if (specSnap[binst] != visitedBlocks.size()) {
        dynamicYes++;
        StatsTracker::increaseEle(curBB, 0, true);
        return addSpeculationNode(current, condition, binst, isInternal,
                                  true);
      } else {
        dynamicNo++;
        // then close speculation & do marking as deletion
        txTree->markPathCondition(current, unsatCore);
        return StatePair(&current, 0);
      }
    }
  } else {
    if (SpecStrategyToUse == TIMID) {
      std::set<std::string> vars = extractVarNames(current, binst);
      if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
        independenceYes++;
        StatsTracker::increaseEle(curBB, 0, true);
        StatsTracker::increaseEle(curBB, 2, false);
      } else {
        independenceNo++;
        StatsTracker::increaseEle(curBB, 1, true);
      }
    } else if (SpecStrategyToUse == AGGRESSIVE) {
      // check independency
      std::set<std::string> vars = extractVarNames(current, binst);
      if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
        // open speculation & assume success
        independenceYes++;
        StatsTracker::increaseEle(curBB, 0, true);
        StatsTracker::increaseEle(curBB, 2, false);
        return StatePair(&current, 0);
      } else {
        // open speculation & result may be success or fail
        independenceNo++;
        StatsTracker::increaseEle(curBB, 0, true);
        return addSpeculationNode(current, condition, binst, isInternal,
                                  true);
      }
    } else if (SpecStrategyToUse == CUSTOM) {
      // check independency
      std::set<std::string> vars = extractVarNames(current, binst);
      if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
        // open speculation & assume success
        independenceYes++;
        //          StatsTracker::increaseEle(curBB, 0, true);
        //          StatsTracker::increaseEle(curBB, 2, false);
        return StatePair(&current, 0);
      } else {
        // open speculation & result may be success or fail and Now second
        // check
        independenceNo++;
        if (specSnap[binst] != visitedBlocks.size()) {
          dynamicYes++;
          StatsTracker::increaseEle(curBB, 0, true);
          return addSpeculationNode(current, condition, binst, isInternal,
                                    true);
        } else {
          dynamicNo++;
          // then close speculation & do marking as deletion
          txTree->markPathCondition(current, unsatCore);
          return StatePair(&current, 0);
        }
      }
    }
  }
}

This is in speculationFork

if (INTERPOLATION_ENABLED && SpecTypeToUse != NO_SPEC &&
    TxSpeculationHelper::isStateSpeculable(current)) {
  if (SpecStrategyToUse == TIMID) {
    // do nothing
  } else if (SpecStrategyToUse == AGGRESSIVE) {
    // open speculation & result may be success or fail
    return addSpeculationNode(current, condition, binst, isInternal, true);
  } else if (SpecStrategyToUse == CUSTOM) {

    std::set<std::string> vars = extractVarNames(current, binst);
    if (TxSpeculationHelper::isIndependent(vars, bbOrderToSpecAvoid)) {
      // open speculation & assume success
      //          independenceYes++;
      return StatePair(&current, 0);
    } else {
      //          independenceNo++;
      // open speculation & result may be success or fail
      if (specSnap[binst] != visitedBlocks.size()) {
        //            dynamicYes++;
        return addSpeculationNode(current, condition, binst, isInternal,
                                  true);
      } else {
        //            dynamicNo++;
        // then close speculation & do marking as deletion
        txTree->markPathCondition(current, unsatCore);
        return StatePair(&current, 0);
      }
    }
  }
}

[sanghu1790]

@xuanlinhha Thanks linh. I read the code and understood the coding part. And it is as same as what you mentioned and I concluded. At least we are on same page. I am fine with the coverage part which is my interpretation says, and I remember this. But for safety part, I am really not able to re-call our discussion. Still, I am thinking why we are doing in such a way. This is also, little unlikely in for safety strategy in branchFork for CUSTOM version, that you have "dynamic checks" without "independence checks". How it is useful, I am not able to understand?

@xuanlinhha Also, linh which part of code is for "new basic-block check" which is different in safety and coverage?

[xuanlinhha]

@sanghu1790 it is in executeInstruction function:

if (SpecTypeToUse == COVERAGE) {
      llvm::BasicBlock *currentBB = state.txTreeNode->getBasicBlock();
      if (visitedBlocks.find(currentBB) == visitedBlocks.end()) {
        if (specFailNew.find(pp) != specFailNew.end()) {
          specFailNew[pp] = specFailNew[pp] + 1;
        } else {
          specFailNew[pp] = 1;
        }
        // check interpolation at is program point
        bool hasInterpolation = TxSubsumptionTable::hasInterpolation(state);
        if (!hasInterpolation) {
          if (specFailNoInter.find(pp) != specFailNoInter.end()) {
            specFailNoInter[pp] = specFailNoInter[pp] + 1;
          } else {
            specFailNoInter[pp] = 1;
          }
        }
        // add to visited BB
        // This is disabled to not to count blocks in speculation subtree
        // visitedBlocks.insert(currentBB);
        specFail++;
        speculativeBackJump(state);
        return;
      }
    }
  }

[rasoolmaghareh]

This is our strategies for spec-coverage: Timid: Check independence, if yes then open speculation & assume success. If dependent, then perform marking similar to deletion. Aggressive: Check independence, if yes then open speculation & assume success. If dependent then open speculation and speculation's result may be success or fail (do marking if fail). Custom: Check independence, if yes then open speculation & assume success. If no then do the second check (check if the coverage has changed since the last speculation at this node). If the second check is satisfied then open speculation & result may be success or fail; else if the second check is not satisfied then close speculation & do marking as deletion.

From these, it is obvious for me that the independence check should not be in safety mode since it is possible that an independence check might say yes for a subtree that contains memory errors (where speculation should have failed) and it reports success. Please let me know if you agree with this @xuanlinhha @sanghu1790 and I will then proceed to the second check.

[sanghu1790]

HI @rasoolmaghareh @xuanlinhha Thanks for your messages.

1. @rasoolmaghareh from your last paragraph of previous message, it is not clear that you are talking about the "independence check" in branchFork or speculationFork when the spec type is safety.
2. If I assume irrespective of branchFork or speculationFork, you dont want to do "independence check". Then there is an ambiguity. CUSTOM has "independence check" in speculationFork but not in branchFork. Which I dont think is correct.
3. For easy understanding of speculation types, versions, checks, I have prepared a matrix in this file Speculation - MATRIX.pdf
4. If I consider your point @rasoolmaghareh for safety, then all the time we never need to supply any Spec_Avoid files. If we dont supply Spec_Avoid files then why in speculationFork we have "Independence Check" for CUSTOM.
5. BTW, @xuanlinhha you have not provided the option of "-spec-type" in speculationFork. The speculationFork code is common for both safety and coverage types. Are you aware about this?
6. @rasoolmaghareh Regarding, "dynamic check" in branchFork and speculationFork I am fine, because I remember this decision we took that without "Independence Check" we can do "dynamic check". So, I dont have any issues.
7. @rasoolmaghareh @xuanlinhha If we are completely agree that in safety type we dont required any Spec_Avoid file then we need to remove the checks from speculationFork when it is safety mode for CUSTOM. We need to discuss on this.
8. Now for Coverage type, I am pretty fine with the independence checks in branchFork for all three versions as coded.
9. Now, currently we have only independence checks in CUSTOM not in TIMID and AGGRESSIVE, which is again ok as we decided.
10. But, here I am proposing one new thing that to implement one command line option for enabling/disabling "independence check" within "speculationFork" for TIMID, AGGRESSIVE, CUSTOM, because I remember for some programs disabling this check outperform and some time enabling this gives good results. So we can have both options to do. Please note that, I am saying to implement only for speculationFork not for branchFork. For branchFork the "independence check" should be compulsory.

If you want we can discuss above points for more clarifications.

Thanks, Sanghu

[xuanlinhha]

so now do we need to change codes following the matrix from @sanghu1790 or you need to discuss with Joxan again?

[sanghu1790]

@xuanlinhha To make it more clear, the MATRIX I made from above the above code you posted. It is not my proposed one. We need to discuss on the definition and MATRIX. Whether the current code is aligned with the definitions or not

[xuanlinhha]

I see @sanghu1790

[rasoolmaghareh]

@xuanlinhha Can you please confirm that the Matrix is inline with the code?

[xuanlinhha]

yes, the matrix from @sanghu1790 is correct

[sanghu1790]

Thanks to both of you @rasoolmaghareh and @xuanlinhha . Now, It will be easy for us to fix the issue.

[rasoolmaghareh]

This is my suggestion @xuanlinhha @sanghu1790:

1- We drop independence check since it is unsound in -spec-type=safety. 2- Since Timid in -spec-type=safety becomes very similar to aggressive, I suggest we drop timid:

[sanghu1790]

@rasoolmaghareh Yes I do agree with you

@xuanlinhha Linh, lets fix this issues first by dropping timid in safety. Secondly. Kindly remove the "Independence check" from speculationFork when type is safety. Third point is to provide one command option to enable/disable "Independence check" in speculationFork for coverage type as we discussed.

[rasoolmaghareh]

@xuanlinhha Let's proceed with safety first, then we will address the independence issue, under the issue for speculation coverage (issue #364)

[sanghu1790]

@rasoolmaghareh I agree.

[xuanlinhha]

Hi all, I made a new commit according to the new matrix, can you please check again with the programs you have? Thanks

[rasoolmaghareh]

@xuanlinhha I ran now and it runs correctly for safety (on both aggressive and custom). I am merging the pull request (#365).

Fixed by #365.