From 2cd1c6b8f418a0b215829e8120da6872a072deb1 Mon Sep 17 00:00:00 2001 From: caballa Date: Mon, 18 Sep 2023 09:43:33 -0600 Subject: [PATCH] fix: lowering of unsigned comparisons Added more comments and tests --- lib/Clam/CfgBuilder.cc | 150 ++++++++------ lib/Transforms/LowerUnsignedICmp.cc | 290 ++++++++++++++-------------- tests/mem/lit.local.cfg | 2 +- tests/mem/transfer-lamports-2.c | 113 +++++++++++ tests/mem/transfer-lamports.c | 27 +-- tests/simple/test-bool-1.c | 9 +- tests/simple/test-bool-2.c | 8 +- tests/simple/test-bool-5.c | 6 - tests/simple/test-bool-6.c | 39 ++++ tests/simple/test-unsigned-cmp-2.c | 17 ++ tests/simple/test-unsigned-cmp-3.c | 20 ++ tests/simple/test-unsigned-cmp-4.c | 20 ++ 12 files changed, 472 insertions(+), 229 deletions(-) create mode 100644 tests/mem/transfer-lamports-2.c create mode 100644 tests/simple/test-bool-6.c create mode 100644 tests/simple/test-unsigned-cmp-2.c create mode 100644 tests/simple/test-unsigned-cmp-3.c create mode 100644 tests/simple/test-unsigned-cmp-4.c diff --git a/lib/Clam/CfgBuilder.cc b/lib/Clam/CfgBuilder.cc index 223b0457..2734e363 100644 --- a/lib/Clam/CfgBuilder.cc +++ b/lib/Clam/CfgBuilder.cc @@ -175,23 +175,21 @@ static void havoc(var_t v, std::string comment, basic_block_t &bb, } } +/** + * Translating unsigned comparisons by using select operators + * PRECONDITION: x cmp y, where cmp will be either <= or < + * + * For instance, x u< y will be translated into: + * + * select(x s>= 0, select(y s>= 0, x u< y, true), select(y s>= 0, false, x u< y) + * + * if isNegated is true then we logically negate cmp, true and false +**/ static void unsignedCmpIntoSignOnes(var_t &res, lin_exp_t &op0, lin_exp_t &op1, crabLitFactory &lfac, basic_block_t &bb, - const bool isNegated, const bool isCmpULE) { - // translating unsigned comparisons by using select operators - // x cmp y, where cmp will be either <= or < - // will be translated into: - // if x >= 0 - // if y >= 0 then x cmp y - // else // x >= 0 y < 0 - // false - // else - // if y >= 0 then // x < 0 y >= 0 - // true - // else x cmp y - // reverse cmp, true and false if isNegated is set + const bool isNegated, const bool isNonStrict) { lin_cst_t cmp; - if (isCmpULE) { + if (isNonStrict) { if (!isNegated) cmp = lin_cst_t(op0 <= op1); else @@ -202,70 +200,100 @@ static void unsignedCmpIntoSignOnes(var_t &res, lin_exp_t &op0, lin_exp_t &op1, else cmp = lin_cst_t(op0 >= op1); } + lin_cst_t trueC = !isNegated ? lin_cst_t::get_true() : lin_cst_t::get_false(); + lin_cst_t falseC = !isNegated ? lin_cst_t::get_false() : lin_cst_t::get_true(); lin_cst_t cst_op0 = lin_cst_t(op0 >= 0); lin_cst_t cst_op1 = lin_cst_t(op1 >= 0); + if (cst_op0.is_tautology()) { // if the first operand is >= 0 if (cst_op1.is_tautology()) { // if the second operand is >= 0 + /** + * x u< y + **/ bb.bool_assign(res, cmp); } else if (cst_op1.is_contradiction()) { // if the second operand is < 0 - bb.bool_assign(res, !isNegated ? lin_cst_t::get_false() - : lin_cst_t::get_true()); + /** + * true + **/ + bb.bool_assign(res, trueC); } else { // don't know the value of the second operand - var_t select_cond_1 = lfac.mkBoolVar(); - bb.bool_assign(select_cond_1, cst_op1); - var_t cmp_var = lfac.mkBoolVar(); - bb.bool_assign(cmp_var, cmp); - var_t v_false = lfac.mkBoolVar(); - bb.bool_assign(v_false, !isNegated ? lin_cst_t::get_false() - : lin_cst_t::get_true()); - bb.bool_select(res, select_cond_1, cmp_var, v_false); + /** + * select(y s>= 0, x u< y, true) + **/ + var_t condB = lfac.mkBoolVar(); + bb.bool_assign(condB, cst_op1); + var_t thenB = lfac.mkBoolVar(); + bb.bool_assign(thenB, cmp); + var_t elseB = lfac.mkBoolVar(); + bb.bool_assign(elseB, trueC); + bb.bool_select(res, condB, thenB, elseB); } } else if (cst_op0.is_contradiction()) { // if the first operand is < 0 if (cst_op1.is_tautology()) { // if the second operand is >= 0 - bb.bool_assign(res, !isNegated ? lin_cst_t::get_true() - : lin_cst_t::get_false()); + /** + * false + **/ + bb.bool_assign(res, falseC); } else if (cst_op1.is_contradiction()) { // if the second operand is < 0 + /** + * x u< y + **/ bb.bool_assign(res, cmp); } else { // don't know the value of the second operand - var_t select_cond_1 = lfac.mkBoolVar(); - bb.bool_assign(select_cond_1, cst_op1); - var_t v_true = lfac.mkBoolVar(); - bb.bool_assign(v_true, !isNegated ? lin_cst_t::get_true() - : lin_cst_t::get_false()); - var_t cmp_var = lfac.mkBoolVar(); - bb.bool_assign(cmp_var, cmp); - bb.bool_select(res, select_cond_1, v_true, cmp_var); + /** + * select(y s>= 0, false, x u< y) + **/ + var_t condB = lfac.mkBoolVar(); + bb.bool_assign(condB, cst_op1); + var_t thenB = lfac.mkBoolVar(); + bb.bool_assign(thenB, falseC); + var_t elseB = lfac.mkBoolVar(); + bb.bool_assign(elseB, cmp); + bb.bool_select(res, condB, thenB, elseB); } } else { // don't know the value of the first operand - var_t select_cond_2 = lfac.mkBoolVar(); - var_t op0_ge_0 = lfac.mkBoolVar(); - var_t op0_lt_0 = lfac.mkBoolVar(); - bb.bool_assign(select_cond_2, cst_op0); if (cst_op1.is_tautology()) { // if the second operand is >= 0 - bb.bool_assign(op0_ge_0, cmp); - bb.bool_assign(op0_lt_0, !isNegated ? lin_cst_t::get_true() - : lin_cst_t::get_false()); + /** + * select(x s>= 0, x u< y, false) + **/ + var_t condB = lfac.mkBoolVar(); + bb.bool_assign(condB, cst_op0); + var_t thenB = lfac.mkBoolVar(); + bb.bool_assign(thenB, cmp); + var_t elseB = lfac.mkBoolVar(); + bb.bool_assign(elseB, falseC); + bb.bool_select(res, condB, thenB, elseB); } else if (cst_op1.is_contradiction()) { // if the second operand is < 0 - bb.bool_assign(op0_ge_0, !isNegated ? lin_cst_t::get_false() - : lin_cst_t::get_true()); - bb.bool_assign(op0_lt_0, cmp); + /** + * select(x s>= 0, true, x u< y) + **/ + var_t condB = lfac.mkBoolVar(); + bb.bool_assign(condB, cst_op0); + var_t thenB = lfac.mkBoolVar(); + bb.bool_assign(thenB, trueC); + var_t elseB = lfac.mkBoolVar(); + bb.bool_assign(elseB, cmp); + bb.bool_select(res, condB, thenB, elseB); } else { // don't know the value of those operands, general cases - var_t select_cond_1 = lfac.mkBoolVar(); - bb.bool_assign(select_cond_1, cst_op1); - var_t cmp_var_true = lfac.mkBoolVar(); - bb.bool_assign(cmp_var_true, cmp); - var_t v_false = lfac.mkBoolVar(); - bb.bool_assign(v_false, !isNegated ? lin_cst_t::get_false() - : lin_cst_t::get_true()); - bb.bool_select(op0_ge_0, select_cond_1, cmp_var_true, v_false); - var_t cmp_var_false = lfac.mkBoolVar(); - bb.bool_assign(cmp_var_false, cmp); - var_t v_true = lfac.mkBoolVar(); - bb.bool_assign(v_true, !isNegated ? lin_cst_t::get_true() - : lin_cst_t::get_false()); - bb.bool_select(op0_lt_0, select_cond_1, v_true, cmp_var_false); + /** + * select(x s>= 0, select(y s>= 0, x u< y, true), select(y s>= 0, false, x u< y) + **/ + var_t condB1 = lfac.mkBoolVar(); + bb.bool_assign(condB1, cst_op0); + var_t condB2 = lfac.mkBoolVar(); + bb.bool_assign(condB2, cst_op1); + var_t cmpB = lfac.mkBoolVar(); + bb.bool_assign(cmpB, cmp); + var_t elseB2 = lfac.mkBoolVar(); + bb.bool_assign(elseB2, trueC); + var_t thenB1 = lfac.mkBoolVar(); + bb.bool_select(thenB1, condB2, cmpB, elseB2); + var_t thenB2 = lfac.mkBoolVar(); + bb.bool_assign(thenB2, falseC); + var_t elseB1 = lfac.mkBoolVar(); + bb.bool_select(elseB1, condB2, thenB2, cmpB); + bb.bool_select(res, condB1, thenB1, elseB1); } - bb.bool_select(res, select_cond_2, op0_ge_0, op0_lt_0); } } @@ -332,7 +360,7 @@ static void cmpInstToCrabBool(CmpInst &I, crabLitFactory &lfac, case CmpInst::ICMP_ULT: { if (removeUnsignedCmp) { unsignedCmpIntoSignOnes(lhs, op0, op1, lfac, bb, - false /*isNegated*/, false /* isCmpULE*/); + false /*isNegated*/, false /* isNonStrict*/); } else { CLAM_WARNING("Crab does not support unsigned constraints. Use --crab-lower-unsigned-icmp option"); } @@ -341,7 +369,7 @@ static void cmpInstToCrabBool(CmpInst &I, crabLitFactory &lfac, case CmpInst::ICMP_ULE: { if (removeUnsignedCmp) { unsignedCmpIntoSignOnes(lhs, op0, op1, lfac, bb, - false /*isNegated*/, true /*isCmpULE*/); + false /*isNegated*/, true /*isNonStrict*/); } else { CLAM_WARNING("Crab does not support unsigned constraints. Use --crab-lower-unsigned-icmp option"); } diff --git a/lib/Transforms/LowerUnsignedICmp.cc b/lib/Transforms/LowerUnsignedICmp.cc index 72034302..3592881d 100644 --- a/lib/Transforms/LowerUnsignedICmp.cc +++ b/lib/Transforms/LowerUnsignedICmp.cc @@ -38,7 +38,7 @@ static bool isNonNegIntCst(Value *V) { return (K->getValue().isNonNegative()); return false; } - + static void normalizeCmpInst(CmpInst *I) { switch (I->getPredicate()) { case ICmpInst::ICMP_UGT: @@ -67,146 +67,156 @@ class LowerUnsignedICmp : public FunctionPass { Value *op1 = CI->getOperand(0); Value *op2 = CI->getOperand(1); - bool is_nonneg_op1 = isNonNegIntCst(op1); - bool is_nonneg_op2 = isNonNegIntCst(op2); - - if (is_nonneg_op2 && is_nonneg_op1) { - // -- This should not happen after InstCombine + // op1 is statically known >= 0 + bool isNonNegOp1 = isNonNegIntCst(op1); + // op2 is statically known >= 0 + bool isNonNegOp2 = isNonNegIntCst(op2); + + if (isNonNegOp2 && isNonNegOp1) { + // This should not happen after InstCombine return; } - - if (is_nonneg_op2 || is_nonneg_op1) { - // -- special case: one of the two operands is an integer - // -- constant - - /* For the case %z is constant (the case %y is constant is - symmetric): - - %b = %y ult %z - CONT - | - V - cur: - %b1 = %y geq 0 - br %b1, %bb1, %bb2 - bb1: - %b2 = %y lt %z - br %cont - bb2: - br %cont - cont: - %b = PHI (%b2, %bb1) (true, %bb2) - */ - - // Check whether the non-constant operand is >= 0 - BasicBlock *tt = - BasicBlock::Create(F->getContext(), "TrueLowerICmp", F, cont); - BasicBlock *ff = - BasicBlock::Create(F->getContext(), "FalseLowerICmp", F, cont); - BranchInst::Create(cont, tt); - BranchInst::Create(cont, ff); - CmpInst *NonNegOp1 = - mkNonNegative(is_nonneg_op2 ? op1 : op2, cur->getTerminator()); - cur->getTerminator()->eraseFromParent(); - BranchInst::Create(tt, ff, NonNegOp1, cur); - - // Create signed comparison that will replace the unsigned one - CmpInst *newCI = - CmpInst::Create(Instruction::ICmp, CI->getSignedPredicate(), op1, op2, - CI->getName(), tt->getTerminator()); - - // Insert a phi node just before the unsigned instruction in - // cont - PHINode *PHI = PHINode::Create(CI->getType(), 0, CI->getName(), CI); - PHI->addIncoming(newCI, tt); - if (is_nonneg_op2) { - PHI->addIncoming(ConstantInt::getTrue(newCI->getType()), ff); - } else { - PHI->addIncoming(ConstantInt::getFalse(newCI->getType()), ff); - } - - // Make sure any users of the unsigned comparison is now an - // user of the phi node. - CI->replaceAllUsesWith(PHI); - - // Finally we remove the unsigned instruction - CI->eraseFromParent(); - } else { - // -- general case: both operands are non-constant - - /* - %b = %y ult %z - CONT - | - V - cur: - %b1 = %y geq 0 - br %b1, %bb1, %bb2 - bb1: - %b2 = %z gep 0 - br %b2, %bb3, %cont - bb2: - %b3 = %z gep 0 - br %b3, cont, %bb4 - bb3: - %b4 = %y lt %z - br %cont - bb4: - %b5 = %y lt %z - br %cont - cont: - %b = PHI (%b4, %bb3) (false, %bb1) (true, %bb2) (%b5, %bb4) - - */ - - // Check whether the first operand is >= 0 - BasicBlock *bb1 = - BasicBlock::Create(F->getContext(), "TrueLowerICmp", F, cont); - BasicBlock *bb2 = - BasicBlock::Create(F->getContext(), "FalseLowerICmp", F, cont); - BasicBlock *bb3 = - BasicBlock::Create(F->getContext(), "TrueLowerICmp", F, cont); - BasicBlock *bb4 = - BasicBlock::Create(F->getContext(), "FalseLowerICmp", F, cont); - - CmpInst *b1 = mkNonNegative(op1, cur->getTerminator()); - cur->getTerminator()->eraseFromParent(); - BranchInst::Create(bb1, bb2, b1, cur); - - // Check whether the second operand is >= 0 - CmpInst *b2 = mkNonNegative(op2, bb1); - BranchInst::Create(bb3, cont, b2, bb1); - - // Check whether the second operand is >= 0 - CmpInst *b3 = mkNonNegative(op2, bb2); - BranchInst::Create(cont, bb4, b3, bb2); - - // Create signed comparison that will replace the unsigned one - CmpInst *b4 = CmpInst::Create(Instruction::ICmp, CI->getSignedPredicate(), - op1, op2, CI->getName(), bb3); - BranchInst::Create(cont, bb3); - - // Create signed comparison that will replace the unsigned one - CmpInst *b5 = CmpInst::Create(Instruction::ICmp, CI->getSignedPredicate(), - op1, op2, CI->getName(), bb4); - BranchInst::Create(cont, bb4); - - // Insert a phi node just before the unsigned instruction in - // cont - PHINode *PHI = PHINode::Create(CI->getType(), 0, CI->getName(), CI); - PHI->addIncoming(ConstantInt::getFalse(CI->getType()), bb1); - PHI->addIncoming(ConstantInt::getTrue(CI->getType()), bb2); - PHI->addIncoming(b4, bb3); - PHI->addIncoming(b5, bb4); - - // Make sure any users of the unsigned comparison is now an - // user of the phi node. - CI->replaceAllUsesWith(PHI); - - // Finally we remove the unsigned instruction - CI->eraseFromParent(); - } - totalUnsignedICmpLowered++; + + if (isNonNegOp2 || isNonNegOp1) { + // Special case: one of the two operands is a constant >=0 + /** + * For the case %y is statically known to be >= 0 + * + * Replace %b = %y ult %z with + * + * cur: + * %b1 = %z geq 0 + * br %b1, %bb1, %bb2 + * bb1: + * %b2 = %y lt %z + * br %cont + * bb2: + * br %cont + * cont: + * %b = PHI (%b2, %bb1) (true, %bb2) + * + * + * For the case %z is statically known to be >= 0 + * + * Replace %b = %y ult %z with + * + * cur: + * %b1 = %y geq 0 + * br %b1, %bb1, %bb2 + * bb1: + * %b2 = %y lt %z + * br %cont + * bb2: + * br %cont + * cont: + * %b = PHI (%b2, %bb1) (false, %bb2) + **/ + + // Check whether the non-constant operand is >= 0 + BasicBlock *tt = + BasicBlock::Create(F->getContext(), "TrueLowerICmp", F, cont); + BasicBlock *ff = + BasicBlock::Create(F->getContext(), "FalseLowerICmp", F, cont); + BranchInst::Create(cont, tt); + BranchInst::Create(cont, ff); + CmpInst *NonNegOp1 = + mkNonNegative(isNonNegOp2 ? op1 : op2, cur->getTerminator()); + cur->getTerminator()->eraseFromParent(); + BranchInst::Create(tt, ff, NonNegOp1, cur); + + // Create signed comparison that will replace the unsigned one + CmpInst *newCI = + CmpInst::Create(Instruction::ICmp, CI->getSignedPredicate(), op1, op2, + CI->getName(), tt->getTerminator()); + + // Insert a phi node just before the unsigned instruction in + // cont + PHINode *PHI = PHINode::Create(CI->getType(), 0, CI->getName(), CI); + PHI->addIncoming(newCI, tt); + if (isNonNegOp2) { + // %b = %op1 ult 5 and %op1 is negative + PHI->addIncoming(ConstantInt::getFalse(newCI->getType()), ff); + } else { + // %b = 5 ult %op2 and %op2 is negative + PHI->addIncoming(ConstantInt::getTrue(newCI->getType()), ff); + } + + // Make sure any users of the unsigned comparison is now an + // user of the phi node. + CI->replaceAllUsesWith(PHI); + // Finally we remove the unsigned instruction + CI->eraseFromParent(); + } else { + /** + * Replace %b = %y ult %z with + * + * cur: + * %b1 = %y geq 0 + * br %b1, %bb1, %bb2 + * bb1: + * %b2 = %z gep 0 + * br %b2, %bb3, %cont + * bb2: + * %b3 = %z gep 0 + * br %b3, %cont, %bb4 + * bb3: + * %b4 = %y lt %z + * br %cont + * bb4: + * %b5 = %y lt %z + * br %cont + * cont: + * %b = PHI (%b4, %bb3) (true, %bb1) (false, %bb2) (%b5, %bb4) + **/ + + // Check whether the first operand is >= 0 + BasicBlock *bb1 = + BasicBlock::Create(F->getContext(), "TrueLowerICmp", F, cont); + BasicBlock *bb2 = + BasicBlock::Create(F->getContext(), "FalseLowerICmp", F, cont); + BasicBlock *bb3 = + BasicBlock::Create(F->getContext(), "TrueLowerICmp", F, cont); + BasicBlock *bb4 = + BasicBlock::Create(F->getContext(), "FalseLowerICmp", F, cont); + + CmpInst *b1 = mkNonNegative(op1, cur->getTerminator()); + cur->getTerminator()->eraseFromParent(); + BranchInst::Create(bb1, bb2, b1, cur); + + // Check whether the second operand is >= 0 + CmpInst *b2 = mkNonNegative(op2, bb1); + BranchInst::Create(bb3, cont, b2, bb1); + + // Check whether the second operand is >= 0 + CmpInst *b3 = mkNonNegative(op2, bb2); + BranchInst::Create(cont, bb4, b3, bb2); + + // Create signed comparison that will replace the unsigned one + CmpInst *b4 = CmpInst::Create(Instruction::ICmp, CI->getSignedPredicate(), + op1, op2, CI->getName(), bb3); + BranchInst::Create(cont, bb3); + + // Create signed comparison that will replace the unsigned one + CmpInst *b5 = CmpInst::Create(Instruction::ICmp, CI->getSignedPredicate(), + op1, op2, CI->getName(), bb4); + BranchInst::Create(cont, bb4); + + // Insert a phi node just before the unsigned instruction in + // cont + PHINode *PHI = PHINode::Create(CI->getType(), 0, CI->getName(), CI); + PHI->addIncoming(ConstantInt::getTrue(CI->getType()), bb1); + PHI->addIncoming(ConstantInt::getFalse(CI->getType()), bb2); + PHI->addIncoming(b4, bb3); + PHI->addIncoming(b5, bb4); + + // Make sure any users of the unsigned comparison is now an + // user of the phi node. + CI->replaceAllUsesWith(PHI); + + // Finally we remove the unsigned instruction + CI->eraseFromParent(); + totalUnsignedICmpLowered++; + } } public: @@ -215,7 +225,6 @@ class LowerUnsignedICmp : public FunctionPass { LowerUnsignedICmp() : FunctionPass(ID) {} virtual bool runOnFunction(Function &F) override { - std::vector worklist; for (inst_iterator It = inst_begin(F), E = inst_end(F); It != E; ++It) { Instruction *I = &*It; @@ -244,7 +253,6 @@ class LowerUnsignedICmp : public FunctionPass { processUnsignedICmp(CI); } - // llvm::errs () << F << "\n"; return change; } diff --git a/tests/mem/lit.local.cfg b/tests/mem/lit.local.cfg index 8fe8e8ae..a80caf7d 100644 --- a/tests/mem/lit.local.cfg +++ b/tests/mem/lit.local.cfg @@ -5,4 +5,4 @@ import clam_config config.excludes = [] if clam_config.use_apron == "OFF" and clam_config.use_elina == "OFF": - config.excludes += ['test-mem-15.c'] + config.excludes += ['test-mem-15.c', 'transfer-lamports-2.c'] diff --git a/tests/mem/transfer-lamports-2.c b/tests/mem/transfer-lamports-2.c new file mode 100644 index 00000000..ca6de466 --- /dev/null +++ b/tests/mem/transfer-lamports-2.c @@ -0,0 +1,113 @@ +// RUN: %clam --inline --crab-dom=pk --crab-track=mem --crab-heap-analysis=cs-sea-dsa-types --crab-lower-unsigned-icmp=true --crab-check=assert --crab-disable-warnings --crab-inter --entry=entrypoint "%s" 2>&1 | OutputCheck %s +// CHECK: ^2 Number of total safe checks$ +// CHECK: ^0 Number of total error checks$ +// CHECK: ^0 Number of total warning checks$ + +/** + * @brief A program demonstrating the transfer of lamports + */ + +#include +#include +#include "clam/clam.h" + +typedef struct { + //SolPubkey *key; /** Public key of the account */ + uint64_t *lamports; /** Number of lamports owned by this account */ + uint64_t data_len; /** Length of data in bytes */ + uint8_t *data; /** On-chain data within this account */ + //SolPubkey *owner; /** Program that owns this account */ + uint64_t rent_epoch; /** The epoch at which this account will next owe rent */ + bool is_signer; /** Transaction was signed by this account's key? */ + bool is_writable; /** Is the account writable? */ + bool executable; /** This account's data contains a loaded program (and is now read-only) */ +} SolAccountInfo; + + +typedef struct { + SolAccountInfo* ka; /** Pointer to an array of SolAccountInfo, must already + point to an array of SolAccountInfos */ + uint64_t ka_num; /** Number of SolAccountInfo entries in `ka` */ + const uint8_t *data; /** pointer to the instruction data */ + uint64_t data_len; /** Length in bytes of the instruction data */ + //const SolPubkey *program_id; /** program_id of the currently executing program */ +} SolParameters; + + +extern NONDET_FN_ATTR uint64_t __CVT_nondet_uint64(void); +extern NONDET_FN_ATTR int64_t __CVT_nondet_int64(void); +extern bool __CVT_deserialize(const uint8_t *input, SolParameters *output, uint64_t ka_num); + +#define DESERIALIZE __CVT_deserialize +#define ASSERT __CRAB_assert +#define ASSUME __CRAB_assume +#define SOL_ARRAY_SIZE(a) (sizeof(a) / sizeof(a[0])) +#define ERROR_INVALID_ARGUMENT 9999999 +#define SUCCESS 0 + +uint64_t CVT_nondet_uint64(void) { + int64_t res = __CVT_nondet_int64(); + if (res >= 0) { + return res; + } + ASSUME(0); + return 0; +} + +void init_account(SolAccountInfo *account, uint64_t val) { + *(account->lamports) = val; +} + +void transfer(SolParameters *params, uint64_t k) { + // As part of the program specification the first account is the source + // account and the second is the destination account + SolAccountInfo *source_info = ¶ms->ka[0]; + SolAccountInfo *destination_info = ¶ms->ka[1]; + // Withdraw five lamports from the source + *source_info->lamports -= k; + // Deposit five lamports into the destination + *destination_info->lamports += k; +} + +uint64_t entrypoint(const uint8_t *input) { + + SolAccountInfo accounts[2]; + SolParameters params = (SolParameters){.ka = accounts}; + + if (!DESERIALIZE(input, ¶ms, SOL_ARRAY_SIZE(accounts))) { + return ERROR_INVALID_ARGUMENT; + } + + SolAccountInfo *source_info = ¶ms.ka[0]; + SolAccountInfo *destination_info = ¶ms.ka[1]; + + // Initialization of the source account + { + uint64_t init_val = CVT_nondet_uint64(); + ASSUME(init_val <= 5000); + init_account(source_info, init_val); + } + // Initialization of the destination account + { + uint64_t init_val = CVT_nondet_uint64(); + ASSUME(init_val <= 5000); + init_account(destination_info, init_val); + } + + uint64_t src_lamport_before = *(source_info->lamports); + uint64_t dst_lamport_before = *(destination_info->lamports); + + // actual transaction: transfer val from src to dst + uint64_t val = CVT_nondet_uint64(); + // Make sure that the source has enough funds + ASSUME(src_lamport_before >= val); + transfer(¶ms, val); + + uint64_t src_lamport_after = *(source_info->lamports); + uint64_t dst_lamport_after = *(destination_info->lamports); + + ASSERT(src_lamport_before == src_lamport_after + val); + ASSERT(dst_lamport_after == dst_lamport_before + val); + + return SUCCESS; +} diff --git a/tests/mem/transfer-lamports.c b/tests/mem/transfer-lamports.c index 0628772b..db447b9b 100644 --- a/tests/mem/transfer-lamports.c +++ b/tests/mem/transfer-lamports.c @@ -1,5 +1,5 @@ -// RUN: %clam --inline --crab-dom=zones --crab-track=mem --crab-heap-analysis=cs-sea-dsa-types --crab-lower-unsigned-icmp=true --crab-check=assert --crab-disable-warnings --crab-inter --entry=entrypoint "%s" 2>&1 | OutputCheck %s -// CHECK: ^2 Number of total safe checks$ +// RUN: %clam --inline --crab-dom=pk --crab-track=mem --crab-heap-analysis=cs-sea-dsa-types --crab-lower-unsigned-icmp=true --crab-check=assert --crab-disable-warnings --crab-inter --entry=entrypoint "%s" 2>&1 | OutputCheck %s +// CHECK: ^4 Number of total safe checks$ // CHECK: ^0 Number of total error checks$ // CHECK: ^0 Number of total warning checks$ @@ -54,7 +54,6 @@ uint64_t CVT_nondet_uint64(void) { return 0; } - void init_account(SolAccountInfo *account, uint64_t val) { *(account->lamports) = val; } @@ -64,7 +63,6 @@ void transfer(SolParameters *params, uint64_t k) { // account and the second is the destination account SolAccountInfo *source_info = ¶ms->ka[0]; SolAccountInfo *destination_info = ¶ms->ka[1]; - // Withdraw five lamports from the source *source_info->lamports -= k; // Deposit five lamports into the destination @@ -83,7 +81,6 @@ uint64_t entrypoint(const uint8_t *input) { SolAccountInfo *source_info = ¶ms.ka[0]; SolAccountInfo *destination_info = ¶ms.ka[1]; - // Initialization of the source account { uint64_t init_val = CVT_nondet_uint64(); @@ -98,24 +95,28 @@ uint64_t entrypoint(const uint8_t *input) { } uint64_t src_lamport_before = *(source_info->lamports); - uint64_t dst_lamport_before = *(destination_info->lamports); + uint64_t dst_lamport_before = *(destination_info->lamports); // actual transaction: transfer val from src to dst uint64_t val = CVT_nondet_uint64(); - ASSUME(val <= 1000); + // Make sure that the source has enough funds + ASSUME(src_lamport_before >= val); + + // Make it a constant value so that zones can handle + // *source_info->lamports -= k which is translated to + // tmp2 := load_from_mem(...); + // tmp1 = tmp2 - k + // store_to_mem(...,tmp1); + ASSUME(val == 100); transfer(¶ms, val); - uint64_t src_lamport_after = *(source_info->lamports); uint64_t dst_lamport_after = *(destination_info->lamports); - // provable with zones ASSERT(src_lamport_before >= src_lamport_after); ASSERT(dst_lamport_before <= dst_lamport_after); - - // provable with pk - //ASSERT(src_lamport_before == src_lamport_after + val); - //ASSERT(dst_lamport_after == dst_lamport_before + val); + ASSERT(src_lamport_before == src_lamport_after + val); + ASSERT(dst_lamport_after == dst_lamport_before + val); return SUCCESS; } diff --git a/tests/simple/test-bool-1.c b/tests/simple/test-bool-1.c index 5297c40c..fc08968e 100644 --- a/tests/simple/test-bool-1.c +++ b/tests/simple/test-bool-1.c @@ -1,8 +1,8 @@ // RUN: %clam -O0 --lower-unsigned-icmp --crab-dom=int --crab-check=assert "%s" 2>&1 | OutputCheck %s // RUN: %clam -O0 --crab-lower-unsigned-icmp --crab-dom=int --crab-check=assert "%s" 2>&1 | OutputCheck %s -// CHECK: ^2 Number of total safe checks$ +// CHECK: ^1 Number of total safe checks$ // CHECK: ^0 Number of total error checks$ -// CHECK: ^0 Number of total warning checks$ +// CHECK: ^1 Number of total warning checks$ #include #include @@ -18,7 +18,8 @@ int main(void) { __CRAB_assume(x < mmax); - __CRAB_assert(x >= 3); - __CRAB_assert(x <= 9); + __CRAB_assert(x >= 3); // EXPECTED WARNING: this assertion is provable but we need to + // restrict nd_uint8_t(). + __CRAB_assert(x <= 9); // EXPECTED OK return 0; } diff --git a/tests/simple/test-bool-2.c b/tests/simple/test-bool-2.c index 17536309..9e5183df 100644 --- a/tests/simple/test-bool-2.c +++ b/tests/simple/test-bool-2.c @@ -1,6 +1,6 @@ // RUN: %clam -O0 --crab-inter --lower-unsigned-icmp --crab-dom=int --crab-check=assert "%s" 2>&1 | OutputCheck %s // RUN: %clam -O0 --crab-inter --crab-lower-unsigned-icmp --crab-dom=int --crab-check=assert "%s" 2>&1 | OutputCheck %s -// CHECK: ^1 Number of total safe checks$ +// CHECK: ^2 Number of total safe checks$ // CHECK: ^0 Number of total error checks$ // CHECK: ^1 Number of total warning checks$ @@ -24,7 +24,9 @@ int main(void) { __CRAB_assume(x < mmax); - __CRAB_assert(x >= 3); // CAN BE PROVEN - __CRAB_assert(x <= 8); // EXPECTED OK BUT CANNOT BE PROVEN + __CRAB_assert(x >= 3); // EXPECTED OK + __CRAB_assert(x <= 8); // EXPECTED WARNING + __CRAB_assert(x <= 20); // EXPECTED OK + return 0; } diff --git a/tests/simple/test-bool-5.c b/tests/simple/test-bool-5.c index 7212e86a..253c4d5b 100644 --- a/tests/simple/test-bool-5.c +++ b/tests/simple/test-bool-5.c @@ -10,12 +10,6 @@ #include #include "clam/clam.h" -size_t size_t_nd(void) { - int res = nd_int(); - __CRAB_assume(res >= 0); - return res; -} - int main() { bool a = nd_bool(); diff --git a/tests/simple/test-bool-6.c b/tests/simple/test-bool-6.c new file mode 100644 index 00000000..22c1dc46 --- /dev/null +++ b/tests/simple/test-bool-6.c @@ -0,0 +1,39 @@ +// RUN: %clam --crab-dom=zones --crab-track=mem --inline --crab-heap-analysis=cs-sea-dsa --crab-lower-unsigned-icmp=true --crab-check=assert "%s" 2>&1 | OutputCheck %s +// CHECK: ^0 Number of total safe checks$ +// CHECK: ^0 Number of total error checks$ +// CHECK: ^1 Number of total warning checks$ + +#include +#include +#include +#include +#include +#include "clam/clam.h" + +int main() { + + bool b; + int64_t x = nd_int64_t(); + int64_t y = nd_int64_t(); + + __CRAB_assume(x <= y); + __CRAB_assume(y >= 0); + if (x >= 0) { + if (y >= 0) { + b = (x <= y); + } else { + b = true; + } + } else { + if (y >= 0) { + b = false; + } else { + b = (x <= y); + } + } + + // This assertion is not provable e.g., x=-1 and y=1 + __CRAB_assert(b); + + return 0; +} diff --git a/tests/simple/test-unsigned-cmp-2.c b/tests/simple/test-unsigned-cmp-2.c new file mode 100644 index 00000000..0a9bd86f --- /dev/null +++ b/tests/simple/test-unsigned-cmp-2.c @@ -0,0 +1,17 @@ +// RUN: clang -O1 -c -emit-llvm %s -o %s.bc +// RUN: %clam --no-preprocess --crab-dom=int --crab-track=mem --crab-heap-analysis=cs-sea-dsa --crab-lower-unsigned-icmp=true --crab-check=assert %s.bc 2>&1 | OutputCheck %s +// RUN: %clam --no-preprocess --crab-dom=int --crab-track=mem --crab-heap-analysis=cs-sea-dsa --lower-unsigned-icmp --crab-check=assert %s.bc 2>&1 | OutputCheck %s +// CHECK: ^0 Number of total safe checks$ +// CHECK: ^0 Number of total error checks$ +// CHECK: ^1 Number of total warning checks$ + +extern void __VERIFIER_assume(int cond); +extern int __VERIFIER_nondet_int(void); +extern void __CRAB_assert(int cond); + +int main(void) { + int x = __VERIFIER_nondet_int(); + __VERIFIER_assume(x < 8561 && x > 2097152UL); + __CRAB_assert(0); // EXPECTED WARNING + return 0; +} diff --git a/tests/simple/test-unsigned-cmp-3.c b/tests/simple/test-unsigned-cmp-3.c new file mode 100644 index 00000000..a9a6932b --- /dev/null +++ b/tests/simple/test-unsigned-cmp-3.c @@ -0,0 +1,20 @@ +// RUN: clang -O1 -c -emit-llvm %s -o %s.bc +// RUN: %clam --no-preprocess --crab-dom=zones --crab-track=mem --crab-heap-analysis=cs-sea-dsa --crab-lower-unsigned-icmp=true --crab-check=assert %s.bc 2>&1 | OutputCheck %s +// RUN: %clam --no-preprocess --crab-dom=zones --crab-track=mem --crab-heap-analysis=cs-sea-dsa --lower-unsigned-icmp --crab-check=assert %s.bc 2>&1 | OutputCheck %s +// CHECK: ^1 Number of total safe checks$ +// CHECK: ^0 Number of total error checks$ +// CHECK: ^0 Number of total warning checks$ + +extern void __VERIFIER_assume(int cond); +extern int __VERIFIER_nondet_int(void); +extern void __CRAB_assert(int cond); + +int main(void) { + + int x = __VERIFIER_nondet_int(); + int y = __VERIFIER_nondet_int(); + __VERIFIER_assume(x < 8561 && x> -2000); + __VERIFIER_assume(x == 10000); + __CRAB_assert(0); // EXPECTED SAFE + return 0; +} diff --git a/tests/simple/test-unsigned-cmp-4.c b/tests/simple/test-unsigned-cmp-4.c new file mode 100644 index 00000000..b59b56a2 --- /dev/null +++ b/tests/simple/test-unsigned-cmp-4.c @@ -0,0 +1,20 @@ +// RUN: clang -O1 -c -emit-llvm %s -o %s.bc +// RUN: %clam --no-preprocess --crab-dom=zones --crab-track=mem --crab-heap-analysis=cs-sea-dsa --crab-lower-unsigned-icmp=true --crab-check=assert %s.bc 2>&1 | OutputCheck %s +// RUN: %clam --no-preprocess --crab-dom=zones --crab-track=mem --crab-heap-analysis=cs-sea-dsa --lower-unsigned-icmp --crab-check=assert %s.bc 2>&1 | OutputCheck %s +// CHECK: ^0 Number of total safe checks$ +// CHECK: ^0 Number of total error checks$ +// CHECK: ^1 Number of total warning checks$ + +extern void __VERIFIER_assume(int cond); +extern int __VERIFIER_nondet_int(void); +extern void __CRAB_assert(int cond); + +int main(void) { + + int x = __VERIFIER_nondet_int(); + int y = __VERIFIER_nondet_int(); + __VERIFIER_assume(x < 8561 && x> -2000); + __VERIFIER_assume(x == 6000); + __CRAB_assert(0); // EXPECTED FALSE + return 0; +}