@@ -116,6 +116,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
116116 add (" klee_is_symbolic" , handleIsSymbolic, true ),
117117 add (" klee_make_symbolic" , handleMakeSymbolic, false ),
118118 add (" klee_make_mock" , handleMakeMock, false ),
119+ add (" klee_make_mock_all" , handleMakeMockAll, false ),
119120 add (" klee_mark_global" , handleMarkGlobal, false ),
120121 add (" klee_prefer_cex" , handlePreferCex, false ),
121122 add (" klee_posix_prefer_cex" , handlePosixPreferCex, false ),
@@ -1077,6 +1078,71 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state,
10771078 }
10781079}
10791080
1081+ void SpecialFunctionHandler::handleMakeMockAll (
1082+ ExecutionState &state, KInstruction *target,
1083+ std::vector<ref<Expr>> &arguments) {
1084+ std::string name;
1085+
1086+ if (arguments.size () != 2 ) {
1087+ executor.terminateStateOnUserError (state,
1088+ " Incorrect number of arguments to "
1089+ " klee_make_mock_all(void*, char*)" );
1090+ return ;
1091+ }
1092+
1093+ name = arguments[1 ]->isZero ()
1094+ ? " "
1095+ : readStringAtAddress (state, executor.makePointer (arguments[1 ]));
1096+
1097+ if (name.empty ()) {
1098+ executor.terminateStateOnUserError (
1099+ state, " Empty name of function in klee_make_mock_all" );
1100+ return ;
1101+ }
1102+
1103+ KFunction *kf = target->parent ->parent ;
1104+
1105+ Executor::ExactResolutionList rl;
1106+ executor.resolveExact (state, arguments[0 ],
1107+ executor.typeSystemManager ->getUnknownType (), rl,
1108+ " make_symbolic" );
1109+
1110+ for (auto &it : rl) {
1111+ ObjectPair op = it.second ->addressSpace .findObject (it.first );
1112+ const MemoryObject *mo = op.first ;
1113+ mo->setName (name);
1114+ mo->updateTimestamp ();
1115+
1116+ const ObjectState *old = op.second ;
1117+ ExecutionState *s = it.second ;
1118+
1119+ if (old->readOnly ) {
1120+ executor.terminateStateOnUserError (
1121+ *s, " cannot make readonly object symbolic" );
1122+ return ;
1123+ }
1124+
1125+ ref<SymbolicSource> source;
1126+ switch (executor.interpreterOpts .MockStrategy ) {
1127+ case MockStrategyKind::Naive:
1128+ source =
1129+ SourceBuilder::mockNaive (executor.kmodule .get (), *kf->function (),
1130+ executor.updateNameVersion (state, name));
1131+ break ;
1132+ case MockStrategyKind::Deterministic:
1133+ std::vector<ref<Expr>> args (kf->getNumArgs ());
1134+ for (size_t i = 0 ; i < kf->getNumArgs (); i++) {
1135+ args[i] = executor.getArgumentCell (state, kf, i).value ;
1136+ }
1137+ source = SourceBuilder::mockDeterministic (executor.kmodule .get (),
1138+ *kf->function (), args);
1139+ break ;
1140+ }
1141+ executor.executeMakeSymbolic (state, mo, old->getDynamicType (), source,
1142+ false );
1143+ }
1144+ }
1145+
10801146void SpecialFunctionHandler::handleMarkGlobal (
10811147 ExecutionState &state, KInstruction *target,
10821148 std::vector<ref<Expr>> &arguments) {
@@ -1231,6 +1297,11 @@ void SpecialFunctionHandler::handleAddTaint(klee::ExecutionState &state,
12311297 " klee_add_taint(void*, size_t)" );
12321298 return ;
12331299 }
1300+
1301+ // uint64_t taintSource = dyn_cast<ConstantExpr>(arguments[1])->getZExtValue();
1302+ // printf("klee_add_taint source: %zu\n", taintSource);
1303+ // executor.executeChangeTaintSource(
1304+ // state, target, executor.makePointer(arguments[0]), taintSource, true);
12341305}
12351306
12361307void SpecialFunctionHandler::handleClearTaint (
@@ -1242,6 +1313,11 @@ void SpecialFunctionHandler::handleClearTaint(
12421313 " klee_clear_taint(void*, size_t)" );
12431314 return ;
12441315 }
1316+
1317+ // uint64_t taintSource = dyn_cast<ConstantExpr>(arguments[1])->getZExtValue();
1318+ // printf("klee_clear_taint source: %zu\n", taintSource);
1319+ // executor.executeChangeTaintSource(
1320+ // state, target, executor.makePointer(arguments[0]), taintSource, false);
12451321}
12461322
12471323void SpecialFunctionHandler::handleCheckTaintSource (
@@ -1255,8 +1331,9 @@ void SpecialFunctionHandler::handleCheckTaintSource(
12551331 }
12561332
12571333// uint64_t taintSource = dyn_cast<ConstantExpr>(arguments[1])->getZExtValue();
1258- // executor.executeCheckTaintSource(state, target,
1259- // executor.makePointer(arguments[0]), taintSource);
1334+ // printf("klee_check_taint_source source: %zu\n", taintSource);
1335+ // executor.executeCheckTaintSource(
1336+ // state, target, executor.makePointer(arguments[0]), taintSource);
12601337}
12611338
12621339void SpecialFunctionHandler::handleGetTaintRule (
@@ -1269,11 +1346,12 @@ void SpecialFunctionHandler::handleGetTaintRule(
12691346 return ;
12701347 }
12711348
1272- // // TODO: now mock
1273- ref<Expr> result = ConstantExpr::create (1 , Expr::Int64);
1274- executor.bindLocal (target, state, result);
1349+ // // TODO: now mock
1350+ ref<Expr> result = ConstantExpr::create (1 , Expr::Int64);
1351+ executor.bindLocal (target, state, result);
12751352
12761353// uint64_t taintSink = dyn_cast<ConstantExpr>(arguments[1])->getZExtValue();
1354+ // printf("klee_get_taint_rule source: %zu\n", taintSink);
12771355// executor.executeGetTaintRule(state, target,
12781356// executor.makePointer(arguments[0]), taintSink);
12791357}
@@ -1287,7 +1365,7 @@ void SpecialFunctionHandler::handleTaintHit(klee::ExecutionState &state,
12871365 return ;
12881366 }
12891367
1290- uint64_t ruleId = dyn_cast<ConstantExpr>(arguments[0 ])->getZExtValue ();
1291- // printf("klee_taint_hit for rule: %zu\n", ruleId );
1292- executor.terminateStateOnTargetTaintError (state, ruleId );
1368+ uint64_t taintRule = dyn_cast<ConstantExpr>(arguments[0 ])->getZExtValue ();
1369+ printf (" klee_taint_hit rule: %zu\n " , taintRule );
1370+ executor.terminateStateOnTargetTaintError (state, taintRule );
12931371}
0 commit comments