@@ -161,59 +161,107 @@ void MockBuilder::buildCallKleeMakeSymbolic(
161161 gep});
162162}
163163
164- inline bool isPointer (const std::vector<Annotation::StatementPtr> &statements) {
164+ inline llvm::Value *
165+ MockBuilder::goByOffset (llvm::Value *value,
166+ const std::vector<std::string> &offset) {
167+ llvm::Value *current = value;
168+ for (const auto &inst : offset) {
169+ if (inst == " *" ) {
170+ if (!current->getType ()->isPointerTy ()) {
171+ klee_error (" Incorrect annotation offset." );
172+ }
173+ current = builder->CreateLoad (current);
174+ } else if (inst == " &" ) {
175+ auto addr = builder->CreateAlloca (current->getType ());
176+ current = builder->CreateStore (current, addr);
177+ } else {
178+ const size_t index = std::stol (inst);
179+ if (!(current->getType ()->isPointerTy () ||
180+ current->getType ()->isArrayTy ())) {
181+ klee_error (" Incorrect annotation offset." );
182+ }
183+ current = builder->CreateConstInBoundsGEP1_64 (current, index);
184+ }
185+ }
186+ return current;
187+ }
188+
189+ inline llvm::Type *getTypeByOffset (llvm::Type *value,
190+ const std::vector<std::string> &offset) {
191+ llvm::Type *current = value;
192+ for (const auto &inst : offset) {
193+ if (inst == " *" ) {
194+ if (!current->isPointerTy ()) {
195+ return nullptr ;
196+ }
197+ current = current->getPointerElementType ();
198+ } else if (inst == " &" ) {
199+ // no needed
200+ } else {
201+ const size_t index = std::stol (inst);
202+ if (current->isArrayTy () || current->isPointerTy ()) {
203+ current = current->getContainedType (index);
204+ } else {
205+ return nullptr ;
206+ }
207+ }
208+ }
209+ return current;
210+ }
211+
212+ inline bool
213+ isCorrectStatements (const std::vector<Annotation::StatementPtr> &statements,
214+ const llvm::Argument *arg) {
165215 return std::any_of (statements.begin (), statements.end (),
166- [](const Annotation::StatementPtr &statement) {
216+ [arg](const Annotation::StatementPtr &statement) {
217+ auto argType =
218+ getTypeByOffset (arg->getType (), statement->offset );
167219 switch (statement->getStatementKind ()) {
168220 case Annotation::StatementKind::Deref:
169221 case Annotation::StatementKind::InitNull:
170- return true ;
222+ return argType-> isPointerTy () ;
171223 case Annotation::StatementKind::Unknown:
172224 default :
173- return false ;
225+ return true ;
174226 }
175227 });
176228}
177229
178230bool tryAllign (
179231 llvm::Function *func,
180- const std::vector<std::vector<Annotation::StatementPtr>> statements,
232+ const std::vector<std::vector<Annotation::StatementPtr>> & statements,
181233 std::vector<std::vector<Annotation::StatementPtr>> &res) {
182234 if (func->arg_size () == statements.size ()) {
183235 return true ;
184236 }
185237
186238 for (size_t i = 0 , j = 0 ; j < func->arg_size () && i < statements.size ();) {
187- if (isPointer (statements[i])) {
188- while (j < func->arg_size () &&
189- !func->getArg (j)->getType ()->isPointerTy ()) { // TODO: add check
190- res.emplace_back ();
191- j++;
192- }
239+ while (isCorrectStatements (statements[i], func->getArg (j))) {
240+ res.emplace_back ();
241+ j++;
193242 if (j >= func->arg_size ()) {
194243 break ;
195244 }
196- res.push_back (statements[i]);
197- } else {
198- res.push_back (statements[i]);
199245 }
246+ res.push_back (statements[i]);
200247 j++;
201248 i++;
202249 }
203250 if (func->arg_size () == statements.size ()) {
204251 return true ;
205252 }
206-
207253 return false ;
208254}
209255
210256void MockBuilder::buildAnnotationForExternalFunctionParams (
211257 llvm::Function *func,
212- const std::vector<std::vector<Annotation::StatementPtr>> &statements) {
213- std::vector<std::vector<Annotation::StatementPtr>> res;
214- bool flag = tryAllign (func, statements, res);
258+ const std::vector<std::vector<Annotation::StatementPtr>>
259+ &statementsNotAllign) {
260+ std::vector<std::vector<Annotation::StatementPtr>> statements;
261+ bool flag = tryAllign (func, statementsNotAllign, statements);
215262 if (!flag) {
216- klee_warning (" Can't use annotation incorrect arguments count" );
263+ klee_warning (" Annotation: incorrect arguments count function %s " ,
264+ func->getName ().str ().c_str ());
217265 return ;
218266 }
219267 for (size_t i = 0 ; i < statements.size (); i++) {
@@ -223,7 +271,7 @@ void MockBuilder::buildAnnotationForExternalFunctionParams(
223271 switch (statement->getStatementKind ()) {
224272 case Annotation::StatementKind::Deref: {
225273 if (!elem->getType ()->isPointerTy ()) {
226- klee_error (" Incorrect annotation deref: arg not pointer" );
274+ klee_error (" Annotation: deref arg not pointer" );
227275 }
228276
229277 std::string derefCondName = " condition_deref_arg_" + std::to_string (i) +
@@ -245,8 +293,6 @@ void MockBuilder::buildAnnotationForExternalFunctionParams(
245293 builder->CreateCondBr (brValue, derefBB, contBB);
246294
247295 builder->SetInsertPoint (derefBB);
248- // deref
249-
250296 builder->CreateBr (contBB);
251297
252298 newFunc->getBasicBlockList ().push_back (contBB); // emit merge block
@@ -335,28 +381,4 @@ void MockBuilder::buildAnnotationForExternalFunctionProperties(
335381 }
336382}
337383
338- llvm::Value *MockBuilder::goByOffset (llvm::Value *value,
339- const std::vector<std::string> &offset) {
340- llvm::Value *current = value;
341- for (const auto &inst : offset) {
342- if (inst == " *" ) {
343- if (!current->getType ()->isPointerTy ()) {
344- klee_error (" Incorrect annotation offset." );
345- }
346- current = builder->CreateLoad (current);
347- } else if (inst == " &" ) {
348- auto addr = builder->CreateAlloca (current->getType ());
349- current = builder->CreateStore (current, addr);
350- } else {
351- const size_t index = std::stol (inst);
352- if (!(current->getType ()->isPointerTy () ||
353- current->getType ()->isArrayTy ())) {
354- klee_error (" Incorrect annotation offset." );
355- }
356- current = builder->CreateConstInBoundsGEP1_64 (current, index);
357- }
358- }
359- return current;
360- }
361-
362384} // namespace klee
0 commit comments