From 71c4a2318fe39ba41ef3918c7b2d5a2004bbfecb Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:49:57 -0800 Subject: [PATCH 01/20] Replace `++c.begin()` with `std::next(c.begin())` The first expression is broken when increment of an rvalue is not defined, see https://en.cppreference.com/w/cpp/iterator/next. --- lib/AssistDS/Devirt.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/AssistDS/Devirt.cpp b/lib/AssistDS/Devirt.cpp index 99ed0af14..3fe33086e 100644 --- a/lib/AssistDS/Devirt.cpp +++ b/lib/AssistDS/Devirt.cpp @@ -237,7 +237,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector& Targets) { // Set the names of the arguments. // F->arg_begin()->setName("funcPtr"); - for (auto A = ++F->arg_begin(), E = F->arg_end(); A != E; ++A) + for (auto A = std::next(F->arg_begin()), E = F->arg_end(); A != E; ++A) A->setName("arg"); // @@ -263,7 +263,7 @@ Devirtualize::buildBounce (CallSite CS, std::vector& Targets) { std::vector Args; Function::arg_iterator P, PE; FunctionType::param_iterator T, TE; - for (P = ++F->arg_begin(), PE = F->arg_end(), + for (P = std::next(F->arg_begin()), PE = F->arg_end(), T = FT->param_begin(), TE = FT->param_end(); P != PE && T != TE; ++P, ++T) Args.push_back(castTo(&*P, *T, "", BL)); From 09e854a00b6df008488b44d0be71540137dfe2e7 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:44:00 -0800 Subject: [PATCH 02/20] Pass an `AttrBuilder` instead of an `AttributeSet` to `AddArgs` This could probably be done more efficiently. --- lib/AssistDS/GEPExprArgs.cpp | 3 ++- lib/AssistDS/LoadArgs.cpp | 3 ++- lib/AssistDS/StructReturnToPointer.cpp | 6 ++++-- lib/AssistDS/TypeChecks.cpp | 6 ++++-- 4 files changed, 12 insertions(+), 6 deletions(-) diff --git a/lib/AssistDS/GEPExprArgs.cpp b/lib/AssistDS/GEPExprArgs.cpp index 7972d70c5..4577716e7 100644 --- a/lib/AssistDS/GEPExprArgs.cpp +++ b/lib/AssistDS/GEPExprArgs.cpp @@ -118,7 +118,8 @@ bool GEPExprArgs::runOnModule(Module& M) { for (auto II = F->arg_begin(); NI != NewF->arg_end(); ++II, ++NI) { ValueMap[&*II] = &*NI; NI->setName(II->getName()); - NI->addAttr(F->getAttributes().getParamAttributes(II->getArgNo() + 1)); + auto ArgAttrs = AttrBuilder(F->getAttributes().getParamAttributes(II->getArgNo() + 1)); + NI->addAttrs(ArgAttrs); } NewF->setAttributes(NewF->getAttributes().addAttributes( F->getContext(), 0, F->getAttributes().getRetAttributes())); diff --git a/lib/AssistDS/LoadArgs.cpp b/lib/AssistDS/LoadArgs.cpp index 677f73ae1..1394b070a 100644 --- a/lib/AssistDS/LoadArgs.cpp +++ b/lib/AssistDS/LoadArgs.cpp @@ -156,7 +156,8 @@ bool LoadArgs::runOnModule(Module& M) { } ValueMap[&*II] = &*NI; NI->setName(II->getName()); - NI->addAttr(F->getAttributes().getParamAttributes(II->getArgNo() + 1)); + auto ArgAttrs = AttrBuilder(F->getAttributes().getParamAttributes(II->getArgNo() + 1)); + NI->addAttrs(ArgAttrs); ++II; } // Perform the cloning. diff --git a/lib/AssistDS/StructReturnToPointer.cpp b/lib/AssistDS/StructReturnToPointer.cpp index 0cb5869a1..f66b9822a 100644 --- a/lib/AssistDS/StructReturnToPointer.cpp +++ b/lib/AssistDS/StructReturnToPointer.cpp @@ -89,8 +89,10 @@ bool StructRet::runOnModule(Module& M) { ValueMap[&*II] = &*NI; NI->setName(II->getName()); AttributeSet attrs = F->getAttributes().getParamAttributes(II->getArgNo() + 1); - if (!attrs.isEmpty()) - NI->addAttr(attrs); + if (attrs.hasAttributes()) { + auto AB = AttrBuilder(attrs); + NI->addAttrs(AB); + } } // Perform the cloning. SmallVector Returns; diff --git a/lib/AssistDS/TypeChecks.cpp b/lib/AssistDS/TypeChecks.cpp index 904cc3d5f..3e4905897 100644 --- a/lib/AssistDS/TypeChecks.cpp +++ b/lib/AssistDS/TypeChecks.cpp @@ -667,7 +667,8 @@ bool TypeChecks::visitAddressTakenFunction(Module &M, Function &F) { // For each of these also copy attributes ValueMap[&*II] = &*NI; NI->setName(II->getName()); - NI->addAttr(F.getAttributes().getParamAttributes(II->getArgNo()+1)); + AttrBuilder AB{F.getAttributes().getParamAttributes(II->getArgNo()+1)}; + NI->addAttrs(AB); } // 4. Copy over attributes for the function @@ -832,7 +833,8 @@ bool TypeChecks::visitInternalVarArgFunction(Module &M, Function &F) { // For each of these also copy attributes ValueMap[&*II] = &*NI; NI->setName(II->getName()); - NI->addAttr(F.getAttributes().getParamAttributes(II->getArgNo()+1)); + AttrBuilder AB{F.getAttributes().getParamAttributes(II->getArgNo()+1)}; + NI->addAttrs(AB); } // 4. Copy over attributes for the function From 585be7487a850e0e50bec76b22d7951d13cd41a6 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 14:39:41 -0800 Subject: [PATCH 03/20] Fix attribute copying when changing function signatures Originally this code mutated an `AttributeList` once for every argument. Each mutation causes the `AttributeList` to be copied, as `AttributeList` is an immutable data type. Now we only one extra `AttributeList`. Calls to `getParamAttributes` are zero-indexed as of LLVM 5.0. --- lib/AssistDS/GEPExprArgs.cpp | 18 ++++-------- lib/AssistDS/LoadArgs.cpp | 22 +++++--------- lib/AssistDS/StructReturnToPointer.cpp | 19 ++++-------- lib/AssistDS/TypeChecks.cpp | 40 ++++++-------------------- 4 files changed, 26 insertions(+), 73 deletions(-) diff --git a/lib/AssistDS/GEPExprArgs.cpp b/lib/AssistDS/GEPExprArgs.cpp index 4577716e7..289655d05 100644 --- a/lib/AssistDS/GEPExprArgs.cpp +++ b/lib/AssistDS/GEPExprArgs.cpp @@ -153,29 +153,21 @@ bool GEPExprArgs::runOnModule(Module& M) { fargs.at(j)->replaceAllUsesWith(GEP_new); } - // TODO: Should we use attrbuilder? - AttributeSet NewCallPAL=AttributeSet(); - // Get the initial attributes of the call - AttributeSet CallPAL = CI->getAttributes(); + AttributeList CallPAL = CI->getAttributes(); AttributeSet RAttrs = CallPAL.getRetAttributes(); AttributeSet FnAttrs = CallPAL.getFnAttributes(); - if (!RAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),0,RAttrs); SmallVector Args; + SmallVector ArgAttrs; Args.push_back(GEP->getPointerOperand()); + ArgAttrs.push_back(AttributeSet()); for(unsigned j =1;jgetNumOperands();j++) { Args.push_back(CI->getOperand(j)); - // position in the AttributesBuilder - AttributeSet Attrs = CallPAL.getParamAttributes(j); - if (!Attrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),Args.size(),Attrs); + ArgAttrs.push_back(CallPAL.getParamAttributes(j)); } - // Create the new attributes vec. - if (!FnAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),~0, FnAttrs); + auto NewCallPAL = AttributeList::get(F->getContext(), FnAttrs, RAttrs, ArgAttrs); CallInst *CallI = CallInst::Create(NewF,Args,"", CI); CallI->setCallingConv(CI->getCallingConv()); CallI->setAttributes(NewCallPAL); diff --git a/lib/AssistDS/LoadArgs.cpp b/lib/AssistDS/LoadArgs.cpp index 1394b070a..2a3d47d08 100644 --- a/lib/AssistDS/LoadArgs.cpp +++ b/lib/AssistDS/LoadArgs.cpp @@ -178,32 +178,24 @@ bool LoadArgs::runOnModule(Module& M) { LoadInst *LI_new = new LoadInst(fargs.at(argNum), "", InsertPoint); fargs.at(argNum+1)->replaceAllUsesWith(LI_new); } - - //this does not seem to be a good idea - AttributeSet NewCallPAL=AttributeSet(); - + // Get the initial attributes of the call - AttributeSet CallPAL = CI->getAttributes(); + AttributeList CallPAL = CI->getAttributes(); AttributeSet RAttrs = CallPAL.getRetAttributes(); AttributeSet FnAttrs = CallPAL.getFnAttributes(); - if (!RAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),0, RAttrs); - + SmallVector Args; + SmallVector ArgAttrs; for(unsigned j =0;jgetNumArgOperands();j++) { if(j == argNum) { Args.push_back(NewVal); + ArgAttrs.push_back(AttributeSet()); } Args.push_back(CI->getArgOperand(j)); - // position in the NewCallPAL - AttributeSet Attrs = CallPAL.getParamAttributes(j+1); - if (!Attrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),Args.size(), Attrs); + ArgAttrs.push_back(CallPAL.getParamAttributes(j)); } - // Create the new attributes vec. - if (!FnAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),~0, FnAttrs); + auto NewCallPAL = AttributeList::get(F->getContext(), FnAttrs, RAttrs, ArgAttrs); CallInst *CallI = CallInst::Create(NewF,Args,"", CI); CallI->setCallingConv(CI->getCallingConv()); CallI->setAttributes(NewCallPAL); diff --git a/lib/AssistDS/StructReturnToPointer.cpp b/lib/AssistDS/StructReturnToPointer.cpp index f66b9822a..365aef0ef 100644 --- a/lib/AssistDS/StructReturnToPointer.cpp +++ b/lib/AssistDS/StructReturnToPointer.cpp @@ -146,30 +146,21 @@ bool StructRet::runOnModule(Module& M) { continue; AllocaInst *AllocaNew = new AllocaInst(F->getReturnType(), 0, "", CI); SmallVector Args; - - //this should probably be done in a different manner - AttributeSet NewCallPAL=AttributeSet(); + SmallVector ArgAttrs; // Get the initial attributes of the call - AttributeSet CallPAL = CI->getAttributes(); + AttributeList CallPAL = CI->getAttributes(); AttributeSet RAttrs = CallPAL.getRetAttributes(); AttributeSet FnAttrs = CallPAL.getFnAttributes(); - if (!RAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),0, RAttrs); - Args.push_back(AllocaNew); + ArgAttrs.push_back(AttributeSet()); for(unsigned j = 0; j < CI->getNumOperands()-1; j++) { Args.push_back(CI->getOperand(j)); - // position in the NewCallPAL - AttributeSet Attrs = CallPAL.getParamAttributes(j); - if (!Attrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),Args.size(), Attrs); + ArgAttrs.push_back(CallPAL.getParamAttributes(j)); } - // Create the new attributes vec. - if (!FnAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F->getContext(),~0, FnAttrs); + auto NewCallPAL = AttributeList::get(F->getContext(), FnAttrs, RAttrs, ArgAttrs); CallInst *CallI = CallInst::Create(NF, Args, "", CI); CallI->setCallingConv(CI->getCallingConv()); CallI->setAttributes(NewCallPAL); diff --git a/lib/AssistDS/TypeChecks.cpp b/lib/AssistDS/TypeChecks.cpp index 3e4905897..bad057bf8 100644 --- a/lib/AssistDS/TypeChecks.cpp +++ b/lib/AssistDS/TypeChecks.cpp @@ -1046,38 +1046,26 @@ bool TypeChecks::visitInternalByValFunction(Module &M, Function &F) { if(InvokeInst *II = dyn_cast(*ui)) { if(II->getCalledFunction() == &F) { SmallVector Args; - - // TODO: not a good idea: - AttributeSet NewCallPAL=AttributeSet(); + SmallVector ArgAttrs; // Get the initial attributes of the call - AttributeSet CallPAL = II->getAttributes(); + AttributeList CallPAL = II->getAttributes(); AttributeSet RAttrs = CallPAL.getRetAttributes(); AttributeSet FnAttrs = CallPAL.getFnAttributes(); - if (!RAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F.getContext() ,0, RAttrs); - Function::arg_iterator NI = F.arg_begin(); for(unsigned j =3;jgetNumOperands();j++, NI++) { // Add the original argument Args.push_back(II->getOperand(j)); + // If there are attributes on this argument, copy them to the correct // position in the NewCallPAL //FIXME: copy the rest of the attributes. if(NI->hasByValAttr()) continue; - AttributeSet Attrs = CallPAL.getParamAttributes(j); - if (!Attrs.isEmpty()) { - NewCallPAL=NewCallPAL.addAttributes(F.getContext(), j, Attrs); - } + ArgAttrs.push_back(CallPAL.getParamAttributes(j)); } - // Create the new attributes vec. - if (!FnAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F.getContext(),~0, FnAttrs); - - // Create the substitute call InvokeInst *CallI = InvokeInst::Create(&F, II->getNormalDest(), @@ -1085,6 +1073,7 @@ bool TypeChecks::visitInternalByValFunction(Module &M, Function &F) { Args, "", II); + auto NewCallPAL = AttributeList::get(F.getContext(), FnAttrs, RAttrs, ArgAttrs); CallI->setCallingConv(II->getCallingConv()); CallI->setAttributes(NewCallPAL); II->replaceAllUsesWith(CallI); @@ -1094,18 +1083,13 @@ bool TypeChecks::visitInternalByValFunction(Module &M, Function &F) { } else if(CallInst *CI = dyn_cast(*ui)) { if(CI->getCalledFunction() == &F) { SmallVector Args; - - // TODO: not a good idea: - AttributeSet NewCallPAL=AttributeSet(); + SmallVector ArgAttrs; // Get the initial attributes of the call - AttributeSet CallPAL = CI->getAttributes(); + AttributeList CallPAL = CI->getAttributes(); AttributeSet RAttrs = CallPAL.getRetAttributes(); AttributeSet FnAttrs = CallPAL.getFnAttributes(); - if (!RAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F.getContext(),0, RAttrs); - Function::arg_iterator II = F.arg_begin(); for(unsigned j =1;jgetNumOperands();j++, II++) { // Add the original argument @@ -1115,21 +1099,15 @@ bool TypeChecks::visitInternalByValFunction(Module &M, Function &F) { //FIXME: copy the rest of the attributes. if(II->hasByValAttr()) continue; - AttributeSet Attrs = CallPAL.getParamAttributes(j); - if (!Attrs.isEmpty()) { - NewCallPAL=NewCallPAL.addAttributes(F.getContext(),j, Attrs); - } + ArgAttrs.push_back(CallPAL.getParamAttributes(j)); } - // Create the new attributes vec. - if (!FnAttrs.isEmpty()) - NewCallPAL=NewCallPAL.addAttributes(F.getContext(),~0, FnAttrs); - // Create the substitute call CallInst *CallI = CallInst::Create(&F, Args, "", CI); + auto NewCallPAL = AttributeList::get(F.getContext(), FnAttrs, RAttrs, ArgAttrs); CallI->setCallingConv(CI->getCallingConv()); CallI->setAttributes(NewCallPAL); CI->replaceAllUsesWith(CallI); From 3d868351bc7ee4e67c89a3f357283d7891091bb8 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:45:13 -0800 Subject: [PATCH 04/20] Replace `HasAttributeSomewhere` with `HasAttribute` --- lib/AssistDS/LoadArgs.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/AssistDS/LoadArgs.cpp b/lib/AssistDS/LoadArgs.cpp index 2a3d47d08..c57e5b67c 100644 --- a/lib/AssistDS/LoadArgs.cpp +++ b/lib/AssistDS/LoadArgs.cpp @@ -80,8 +80,8 @@ bool LoadArgs::runOnModule(Module& M) { // do not care about dead arguments if(ai->use_empty()) continue; - if(F->getAttributes().getParamAttributes(argNum).hasAttrSomewhere(Attribute::SExt) || - F->getAttributes().getParamAttributes(argNum).hasAttrSomewhere(Attribute::ZExt)) + if(F->getAttributes().getParamAttributes(argNum).hasAttribute(Attribute::SExt) || + F->getAttributes().getParamAttributes(argNum).hasAttribute(Attribute::ZExt)) continue; if (isa(CI->getArgOperand(argNum))) break; From d97ad407f3b4d0e781323b3f8ac6c5df19366f42 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:20:15 -0800 Subject: [PATCH 05/20] Pass default address space to `AllocaInst` constructor `AllocaInst` now requires an address space. If a load or store instruction for that data exists, we use that same address space. Otherwise, we use the default address space. --- lib/AssistDS/LoadArgs.cpp | 3 ++- lib/AssistDS/TypeChecks.cpp | 14 +++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/lib/AssistDS/LoadArgs.cpp b/lib/AssistDS/LoadArgs.cpp index c57e5b67c..abd464b59 100644 --- a/lib/AssistDS/LoadArgs.cpp +++ b/lib/AssistDS/LoadArgs.cpp @@ -93,7 +93,8 @@ bool LoadArgs::runOnModule(Module& M) { LoadInst *LI = dyn_cast(CI->getArgOperand(argNum)); Instruction * InsertPt = &(Func->getEntryBlock().front()); - AllocaInst *NewVal = new AllocaInst(LI->getType(), "",InsertPt); + AllocaInst *NewVal = new AllocaInst( + LI->getType(), LI->getPointerAddressSpace(), "", InsertPt); StoreInst *Copy = new StoreInst(LI, NewVal); Copy->insertAfter(LI); diff --git a/lib/AssistDS/TypeChecks.cpp b/lib/AssistDS/TypeChecks.cpp index bad057bf8..cb7faac4a 100644 --- a/lib/AssistDS/TypeChecks.cpp +++ b/lib/AssistDS/TypeChecks.cpp @@ -696,7 +696,7 @@ bool TypeChecks::visitAddressTakenFunction(Module &M, Function &F) { unsigned int i; unsigned int NumArgs = II->getNumOperands() - 3; Value *NumArgsVal = ConstantInt::get(Int32Ty, NumArgs); - AllocaInst *AI = new AllocaInst(TypeTagTy, NumArgsVal, "", &*InsPt); + AllocaInst *AI = new AllocaInst(TypeTagTy, 0, NumArgsVal, "", &*InsPt); // set the metadata for the varargs in AI for(i = 3; i getNumOperands(); i++) { Value *Idx[1]; @@ -733,7 +733,7 @@ bool TypeChecks::visitAddressTakenFunction(Module &M, Function &F) { unsigned int NumArgs = CI->getNumOperands() - 1; inst_iterator InsPt = inst_begin(CI->getParent()->getParent()); Value *NumArgsVal = ConstantInt::get(Int32Ty, NumArgs); - AllocaInst *AI = new AllocaInst(TypeTagTy, NumArgsVal, "", &*InsPt); + AllocaInst *AI = new AllocaInst(TypeTagTy, 0, NumArgsVal, "", &*InsPt); // set the metadata for the varargs in AI for(i = 1; i getNumOperands(); i++) { Value *Idx[1]; @@ -926,7 +926,7 @@ bool TypeChecks::visitInternalVarArgFunction(Module &M, Function &F) { unsigned int i; unsigned int NumArgs = II->getNumOperands() - 3; Value *NumArgsVal = ConstantInt::get(Int32Ty, NumArgs); - AllocaInst *AI = new AllocaInst(TypeTagTy, NumArgsVal, "", &*InsPt); + AllocaInst *AI = new AllocaInst(TypeTagTy, 0, NumArgsVal, "", &*InsPt); // set the metadata for the varargs in AI for(i = 3; i getNumOperands(); i++) { Value *Idx[1]; @@ -959,7 +959,7 @@ bool TypeChecks::visitInternalVarArgFunction(Module &M, Function &F) { unsigned int i; unsigned int NumArgs = CI->getNumArgOperands(); Value *NumArgsVal = ConstantInt::get(Int32Ty, NumArgs); - AllocaInst *AI = new AllocaInst(TypeTagTy, NumArgsVal, "", &*InsPt); + AllocaInst *AI = new AllocaInst(TypeTagTy, 0, NumArgsVal, "", &*InsPt); // set the metadata for the varargs in AI for(i = 0; i getNumArgOperands(); i++) { Value *Idx[1]; @@ -1031,7 +1031,7 @@ bool TypeChecks::visitInternalByValFunction(Module &M, Function &F) { continue; assert(Arg.getType()->isPointerTy()); Type *ETy = (cast(Arg.getType()))->getElementType(); - AllocaInst *AI = new AllocaInst(ETy, "", InsertBefore); + AllocaInst *AI = new AllocaInst(ETy, 0, "", InsertBefore); // Do this before adding the load/store pair, so that those uses are not replaced. Arg.replaceAllUsesWith(AI); LoadInst *LI = new LoadInst(&Arg, "", InsertBefore); @@ -1996,7 +1996,7 @@ bool TypeChecks::visitIndirectCallSite(Module &M, Instruction *I) { CallSite CS = CallSite(I); unsigned int NumArgs = CS.arg_size(); Value *NumArgsVal = ConstantInt::get(Int32Ty, NumArgs); - AllocaInst *AI = new AllocaInst(TypeTagTy, NumArgsVal, "", &*InsPt); + AllocaInst *AI = new AllocaInst(TypeTagTy, 0, NumArgsVal, "", &*InsPt); for(unsigned int i = 0; i < CS.arg_size(); i++) { Value *Idx[1]; Idx[0] = ConstantInt::get(Int32Ty, i-1); @@ -2061,7 +2061,7 @@ bool TypeChecks::visitLoadInst(Module &M, LoadInst &LI) { Value *BCI = castTo(LI.getPointerOperand(), VoidPtrTy, "", &LI); Value *Size = ConstantInt::get(Int32Ty, getSize(LI.getType())); - AllocaInst *AI = new AllocaInst(TypeTagTy, Size, "", &*InsPt); + AllocaInst *AI = new AllocaInst(TypeTagTy, LI.getPointerAddressSpace(), Size, "", &*InsPt); std::vectorArgs1; Args1.push_back(BCI); From b1b3c2afca665003c74f0555131de38d69458bc1 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:16:20 -0800 Subject: [PATCH 06/20] Remove NULL terminator variadic template functions LLVM now uses variadic templates instead of C-style varargs functions. Conflicts: lib/smack/CodifyStaticInits.cpp --- lib/AssistDS/DynCount.cpp | 2 +- lib/AssistDS/SVADevirt.cpp | 3 +- lib/AssistDS/TypeChecks.cpp | 99 ++++++++++++++------------------- lib/AssistDS/TypeChecksOpt.cpp | 30 ++++------ lib/smack/CodifyStaticInits.cpp | 2 +- 5 files changed, 55 insertions(+), 81 deletions(-) diff --git a/lib/AssistDS/DynCount.cpp b/lib/AssistDS/DynCount.cpp index a033f7e2a..de0e0459a 100644 --- a/lib/AssistDS/DynCount.cpp +++ b/lib/AssistDS/DynCount.cpp @@ -128,7 +128,7 @@ Dyncount::runOnModule (Module & M) { : M.getFunction ("MAIN__"); BasicBlock & BB = MainFunc->getEntryBlock(); - Constant * Setup = M.getOrInsertFunction ("DYN_COUNT_setup", Type::getVoidTy(M.getContext()), Total->getType(), Safe->getType(), NULL); + Constant * Setup = M.getOrInsertFunction ("DYN_COUNT_setup", Type::getVoidTy(M.getContext()), Total->getType(), Safe->getType()); std::vector args; args.push_back (Total); args.push_back (Safe); diff --git a/lib/AssistDS/SVADevirt.cpp b/lib/AssistDS/SVADevirt.cpp index 53fe10856..9f7db4cb6 100644 --- a/lib/AssistDS/SVADevirt.cpp +++ b/lib/AssistDS/SVADevirt.cpp @@ -170,8 +170,7 @@ namespace { IndirectFuncFail = M.getOrInsertFunction ("pchk_ind_fail", Type::VoidTy, - PointerType::getUnqual(Type::Int8Ty), - NULL); + PointerType::getUnqual(Type::Int8Ty)); std::set safecalls; std::vector toDelete; diff --git a/lib/AssistDS/TypeChecks.cpp b/lib/AssistDS/TypeChecks.cpp index cb7faac4a..f3ddf7524 100644 --- a/lib/AssistDS/TypeChecks.cpp +++ b/lib/AssistDS/TypeChecks.cpp @@ -383,66 +383,57 @@ void TypeChecks::initRuntimeCheckPrototypes(Module &M) { RegisterArgv = M.getOrInsertFunction("trackArgvType", VoidTy, Int32Ty, /*argc */ - VoidPtrTy->getPointerTo(),/*argv*/ - NULL); + VoidPtrTy->getPointerTo() /*argv*/); RegisterEnvp = M.getOrInsertFunction("trackEnvpType", VoidTy, - VoidPtrTy->getPointerTo(),/*envp*/ - NULL); + VoidPtrTy->getPointerTo() /*envp*/); trackGlobal = M.getOrInsertFunction("trackGlobal", VoidTy, VoidPtrTy,/*ptr*/ TypeTagTy,/*type*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackArray = M.getOrInsertFunction("trackArray", VoidTy, VoidPtrTy,/*ptr*/ Int64Ty,/*size*/ Int64Ty,/*count*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackInitInst = M.getOrInsertFunction("trackInitInst", VoidTy, VoidPtrTy,/*ptr*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackUnInitInst = M.getOrInsertFunction("trackUnInitInst", VoidTy, VoidPtrTy,/*ptr*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackStoreInst = M.getOrInsertFunction("trackStoreInst", VoidTy, VoidPtrTy,/*ptr*/ TypeTagTy,/*type*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); getTypeTag = M.getOrInsertFunction("getTypeTag", VoidTy, VoidPtrTy, /*ptr*/ Int64Ty, /*size*/ TypeTagPtrTy, /*dest for type tag*/ - Int32Ty, /*tag*/ - NULL); + Int32Ty /*tag*/); checkTypeInst = M.getOrInsertFunction("checkType", VoidTy, TypeTagTy,/*type*/ Int64Ty,/*size*/ TypeTagPtrTy,/*ptr to metadata*/ VoidPtrTy,/*ptr*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); setTypeInfo = M.getOrInsertFunction("setTypeInfo", VoidTy, VoidPtrTy,/*dest ptr*/ @@ -450,39 +441,33 @@ void TypeChecks::initRuntimeCheckPrototypes(Module &M) { Int64Ty,/*size*/ TypeTagTy, VoidPtrTy, /*src ptr*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); copyTypeInfo = M.getOrInsertFunction("copyTypeInfo", VoidTy, VoidPtrTy,/*dest ptr*/ VoidPtrTy,/*src ptr*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackStringInput = M.getOrInsertFunction("trackStringInput", VoidTy, VoidPtrTy, - Int32Ty, - NULL); + Int32Ty); setVAInfo = M.getOrInsertFunction("setVAInfo", VoidTy, VoidPtrTy,/*va_list ptr*/ Int64Ty,/*total num of elements in va_list */ TypeTagPtrTy,/*ptr to metadta*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); copyVAInfo = M.getOrInsertFunction("copyVAInfo", VoidTy, VoidPtrTy,/*dst va_list*/ VoidPtrTy,/*src va_list */ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); checkVAArg = M.getOrInsertFunction("checkVAArgType", VoidTy, VoidPtrTy,/*va_list ptr*/ TypeTagTy,/*type*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); } @@ -1207,8 +1192,8 @@ void TypeChecks::print(raw_ostream &OS, const Module *M) const { bool TypeChecks::initShadow(Module &M) { // Create the call to the runtime initialization function and place it before the store instruction. - Constant * RuntimeCtor = M.getOrInsertFunction("tc.init", VoidTy, NULL); - Constant * InitFn = M.getOrInsertFunction("shadowInit", VoidTy, NULL); + Constant * RuntimeCtor = M.getOrInsertFunction("tc.init", VoidTy); + Constant * InitFn = M.getOrInsertFunction("shadowInit", VoidTy); //RuntimeCtor->setDoesNotThrow(); //RuntimeCtor->setLinkage(GlobalValue::InternalLinkage); @@ -1512,7 +1497,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(I); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); Instruction *InsertPt = I; if (InvokeInst *II = dyn_cast(InsertPt)) { @@ -1527,7 +1512,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); Instruction *InsertPt = I; if (InvokeInst *II = dyn_cast(InsertPt)) { @@ -1546,7 +1531,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { Args.push_back(BCI); Args.push_back(BCI_Size); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackaccept", VoidTy, VoidPtrTy,VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackaccept", VoidTy, VoidPtrTy,VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("poll")) { @@ -1556,7 +1541,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { Args.push_back(BCI); Args.push_back(CS.getArgument(1)); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackpoll", VoidTy, VoidPtrTy, Int64Ty, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackpoll", VoidTy, VoidPtrTy, Int64Ty, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("getaddrinfo")) { @@ -1565,7 +1550,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetaddrinfo", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetaddrinfo", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("mmap")) { @@ -1586,7 +1571,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { Args.push_back(BCI_Dest); Args.push_back(BCI_Src); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackStrcpyInst", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackStrcpyInst", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI_Src); } else if (F->getName().str() == std::string("gettimeofday") || @@ -1608,7 +1593,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetpwuid", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetpwuid", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("getpwnam")) { @@ -1617,7 +1602,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetpwuid", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetpwuid", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if(F->getName().str() == std::string("getopt_long")) { @@ -1627,7 +1612,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(LI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(LI); } else if (F->getName().str() == std::string("getgruid") || @@ -1652,7 +1637,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetservbyname", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetservbyname", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("gethostbyname") || @@ -1662,7 +1647,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgethostbyname", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgethostbyname", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("gethostname")) { @@ -1671,7 +1656,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgethostname", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgethostname", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("getenv") || @@ -1682,7 +1667,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("getcwd")) { @@ -1691,7 +1676,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if(F->getName().str() == std::string("crypt")) { @@ -1700,7 +1685,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("getrusage") || @@ -1736,7 +1721,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackctype", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackctype", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("__ctype_toupper_loc")) { @@ -1745,7 +1730,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackctype_32", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackctype_32", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("__ctype_tolower_loc")) { @@ -1754,7 +1739,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackctype_32", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackctype_32", VoidTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); } else if (F->getName().str() == std::string("strtol") || @@ -1776,14 +1761,14 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { Args.push_back(BCI_Dest); Args.push_back(BCI_Src); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackStrcatInst", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackStrcatInst", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty); CallInst::Create(F, Args, "", I); } else if (F->getName().str() == std::string("strcpy")) { std::vector Args; Args.push_back(CS.getArgument(0)); Args.push_back(CS.getArgument(1)); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackStrcpyInst", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackStrcpyInst", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty); CallInst::Create(F, Args, "", I); } else if (F->getName().str() == std::string("strncpy")) { std::vectorArgs; @@ -1791,14 +1776,14 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { Args.push_back(CS.getArgument(1)); Args.push_back(CS.getArgument(2)); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackStrncpyInst", VoidTy, VoidPtrTy, VoidPtrTy, I->getOperand(3)->getType(), Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackStrncpyInst", VoidTy, VoidPtrTy, VoidPtrTy, I->getOperand(3)->getType(), Int32Ty); CallInst::Create(F, Args, "", I); } else if (F->getName().str() == std::string("readlink")) { std::vectorArgs; Args.push_back(CS.getArgument(1)); Args.push_back(I); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackReadLink", VoidTy, VoidPtrTy, I->getType(), Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackReadLink", VoidTy, VoidPtrTy, I->getType(), Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(I); } else if (F->getName().str() == std::string("pipe")) { @@ -1806,7 +1791,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vector Args; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackpipe", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackpipe", VoidTy, VoidPtrTy, Int32Ty); CallInst::Create(F, Args, "", I); return true; } else if (F->getName().str() == std::string("getsockname")) { @@ -1818,7 +1803,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { Args.push_back(BCI); Args.push_back(BCI_Size); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetsockname", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetsockname", VoidTy, VoidPtrTy, VoidPtrTy, Int32Ty); CallInst *CI = CallInst::Create(F, Args); CI->insertAfter(BCI); return true; @@ -1931,7 +1916,7 @@ bool TypeChecks::visitCallSite(Module &M, CallSite CS) { std::vectorArgs; Args.push_back(BCI); Args.push_back(getTagCounter()); - Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty, NULL); + Constant *F = M.getOrInsertFunction("trackgetcwd", VoidTy, VoidPtrTy, Int32Ty); CallInst *CINew = CallInst::Create(F, Args); CINew->insertAfter(I); } else if(F->getName().str() == std::string("sprintf")) { diff --git a/lib/AssistDS/TypeChecksOpt.cpp b/lib/AssistDS/TypeChecksOpt.cpp index 874de2077..490458959 100644 --- a/lib/AssistDS/TypeChecksOpt.cpp +++ b/lib/AssistDS/TypeChecksOpt.cpp @@ -70,49 +70,42 @@ bool TypeChecksOpt::runOnModule(Module &M) { VoidPtrTy, Int8Ty, Int64Ty, - Int32Ty, - NULL); + Int32Ty); trackGlobal = M.getOrInsertFunction("trackGlobal", VoidTy, VoidPtrTy,/*ptr*/ TypeTagTy,/*type*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackInitInst = M.getOrInsertFunction("trackInitInst", VoidTy, VoidPtrTy,/*ptr*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackUnInitInst = M.getOrInsertFunction("trackUnInitInst", VoidTy, VoidPtrTy,/*ptr*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackStoreInst = M.getOrInsertFunction("trackStoreInst", VoidTy, VoidPtrTy,/*ptr*/ TypeTagTy,/*type*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); checkTypeInst = M.getOrInsertFunction("checkType", VoidTy, TypeTagTy,/*type*/ Int64Ty,/*size*/ TypeTagPtrTy, VoidPtrTy,/*ptr*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); copyTypeInfo = M.getOrInsertFunction("copyTypeInfo", VoidTy, VoidPtrTy,/*dest ptr*/ VoidPtrTy,/*src ptr*/ Int64Ty,/*size*/ - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); setTypeInfo = M.getOrInsertFunction("setTypeInfo", VoidTy, VoidPtrTy,/*dest ptr*/ @@ -120,20 +113,17 @@ bool TypeChecksOpt::runOnModule(Module &M) { Int64Ty,/*size*/ TypeTagTy, VoidPtrTy, - Int32Ty,/*tag*/ - NULL); + Int32Ty /*tag*/); trackStringInput = M.getOrInsertFunction("trackStringInput", VoidTy, VoidPtrTy, - Int32Ty, - NULL); + Int32Ty ); getTypeTag = M.getOrInsertFunction("getTypeTag", VoidTy, VoidPtrTy, /*ptr*/ Int64Ty, /*size*/ TypeTagPtrTy, /*dest for type tag*/ - Int32Ty, /*tag*/ - NULL); + Int32Ty /*tag*/); MallocFunc = M.getFunction("malloc"); for(Value::user_iterator User = trackGlobal->user_begin(); User != trackGlobal->user_end(); ++User) { diff --git a/lib/smack/CodifyStaticInits.cpp b/lib/smack/CodifyStaticInits.cpp index 5c92b330f..3db86b593 100644 --- a/lib/smack/CodifyStaticInits.cpp +++ b/lib/smack/CodifyStaticInits.cpp @@ -29,7 +29,7 @@ bool CodifyStaticInits::runOnModule(Module &M) { DSAWrapper *DSA = &getAnalysis(); Function *F = dyn_cast(M.getOrInsertFunction( - Naming::STATIC_INIT_PROC, Type::getVoidTy(C), NULL)); + Naming::STATIC_INIT_PROC, Type::getVoidTy(C))); BasicBlock *B = BasicBlock::Create(C, "entry", F); IRBuilder<> IRB(B); From 9fe94c6897d93d3b4483c74d6efff2bbf36ff551 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Tue, 16 Jul 2019 13:14:02 -0600 Subject: [PATCH 07/20] Updated LLVM version to 5.0 --- bin/versions | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/bin/versions b/bin/versions index c447c59c7..1dead4a48 100644 --- a/bin/versions +++ b/bin/versions @@ -5,6 +5,6 @@ BOOGIE_COMMIT=5c829b6340 CORRAL_COMMIT=c446f5e827 SYMBOOGLIX_COMMIT=7210e5d09b LOCKPWN_COMMIT=73eddf97bd -LLVM_SHORT_VERSION=4.0 -LLVM_FULL_VERSION=4.0.1 +LLVM_SHORT_VERSION=5.0 +LLVM_FULL_VERSION=5.0.2 RUST_VERSION=2016-12-16 From 9206046a6a02ef2d01631b21b80b0838d8ddc7cc Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:52:37 -0800 Subject: [PATCH 08/20] Simplify call to `RemoveAttr` `RemoveAttr` takes an `AttributeKind`. --- lib/AssistDS/TypeChecks.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/lib/AssistDS/TypeChecks.cpp b/lib/AssistDS/TypeChecks.cpp index f3ddf7524..1716a6187 100644 --- a/lib/AssistDS/TypeChecks.cpp +++ b/lib/AssistDS/TypeChecks.cpp @@ -1107,12 +1107,9 @@ bool TypeChecks::visitInternalByValFunction(Module &M, Function &F) { } // remove the byval attribute from the function - AttrBuilder B; - B.addAttribute(Attribute::ByVal); for (Function::arg_iterator I = F.arg_begin(); I != F.arg_end(); ++I) { - if (!I->hasByValAttr()) - continue; - I->removeAttr(AttributeSet::get(M.getContext(),0, B)); + if (I->hasByValAttr()) + I->removeAttr(Attribute::AttrKind::ByVal); } return true; } From e4e593970c8a9f95aca6db05ea0f9b3603fb41a8 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 16:35:28 -0800 Subject: [PATCH 09/20] Use `args` iterators instead of `GetArgumentList` Conflicts: lib/smack/SmackInstGenerator.cpp lib/smack/SmackRep.cpp tools/llvm2bpl/llvm2bpl.cpp --- lib/smack/SmackInstGenerator.cpp | 2 +- lib/smack/SmackRep.cpp | 4 ++-- tools/llvm2bpl/llvm2bpl.cpp | 6 +++--- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 30fd63141..4b9c35be8 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -163,7 +163,7 @@ void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock &bb) { if (SmackOptions::isEntryPoint(naming->get(*F))) { emit(recordProcedureCall( F, {Attr::attr("cexpr", "smack:entry:" + naming->get(*F))})); - for (auto &A : F->getArgumentList()) { + for (auto &A : F->args()) { emit(recordProcedureCall(&A, {Attr::attr("cexpr", "smack:arg:" + naming->get(*F) + diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index e3c1ba466..0f3ee908a 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -956,7 +956,7 @@ ProcDecl *SmackRep::procedure(Function *F, CallInst *CI) { std::list decls; std::list blocks; - for (auto &A : F->getArgumentList()) + for (auto &A : F->args()) params.push_back({naming->get(A), type(A.getType())}); if (!F->getReturnType()->isVoidTy()) @@ -1168,7 +1168,7 @@ unsigned SmackRep::numElements(const llvm::Constant *v) { void SmackRep::addInitFunc(const llvm::Function *f) { assert(f->getReturnType()->isVoidTy() && "Init functions cannot return a value"); - assert(f->getArgumentList().empty() && + assert(f->arg_empty() && "Init functions cannot take parameters"); initFuncs.push_back(naming->get(*f)); } diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index f3f165c44..deec47534 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -209,11 +209,11 @@ int main(int argc, char **argv) { pass_manager.add(new smack::AddTiming()); } - std::vector files; + std::vector files; if (!FinalIrFilename.empty()) { std::error_code EC; - auto F = new tool_output_file(FinalIrFilename.c_str(), EC, sys::fs::F_None); + auto F = new ToolOutputFile(FinalIrFilename.c_str(), EC, sys::fs::F_None); if (EC) check(EC.message()); F->keep(); @@ -223,7 +223,7 @@ int main(int argc, char **argv) { if (!OutputFilename.empty()) { std::error_code EC; - auto F = new tool_output_file(OutputFilename.c_str(), EC, sys::fs::F_None); + auto F = new ToolOutputFile(OutputFilename.c_str(), EC, sys::fs::F_None); if (EC) check(EC.message()); F->keep(); From 423a2ace70d01b5cfed66edbeb54e85b8233baba Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Tue, 13 Nov 2018 21:33:51 -0800 Subject: [PATCH 10/20] Assorted small changes Conflicts: lib/smack/SmackInstGenerator.cpp --- lib/smack/SmackInstGenerator.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index 4b9c35be8..d9133972f 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -288,8 +288,8 @@ void SmackInstGenerator::visitSwitchInst(llvm::SwitchInst &si) { for (llvm::SwitchInst::CaseIt i = si.case_begin(); i != si.case_begin(); ++i) { - const Expr *v = rep->expr(i.getCaseValue()); - targets.push_back({Expr::eq(e, v), i.getCaseSuccessor()}); + const Expr *v = rep->expr(i->getCaseValue()); + targets.push_back({Expr::eq(e, v), i->getCaseSuccessor()}); // Add the negation of this case to the default case n = Expr::and_(n, Expr::neq(e, v)); From 0217717238b029cbc18b19b6c39b72ae9065c8b5 Mon Sep 17 00:00:00 2001 From: Dylan MacKenzie Date: Sat, 17 Nov 2018 12:43:39 -0800 Subject: [PATCH 11/20] Remove uses of `dump()` This method is intended for use in debuggers, and is only available in debug builds of LLVM (which aren't installed by default). Use `print(_, true)` instead, which has the same effect. Perhaps there should be a helper function in smack for this? Conflicts: lib/AssistDS/ArgCast.cpp lib/AssistDS/SimplifyExtractValue.cpp --- lib/AssistDS/ArgCast.cpp | 8 ++++---- lib/AssistDS/DSNodeEquivs.cpp | 2 +- lib/AssistDS/SimplifyExtractValue.cpp | 18 +++++++++--------- lib/DSA/CallTargets.cpp | 2 +- lib/DSA/DataStructure.cpp | 2 +- 5 files changed, 16 insertions(+), 16 deletions(-) diff --git a/lib/AssistDS/ArgCast.cpp b/lib/AssistDS/ArgCast.cpp index cc6813f43..796867b05 100644 --- a/lib/AssistDS/ArgCast.cpp +++ b/lib/AssistDS/ArgCast.cpp @@ -153,8 +153,8 @@ bool ArgCast::runOnModule(Module& M) { } } } else { - SDEBUG(ArgType->dump()); - SDEBUG(FormalType->dump()); + SDEBUG(ArgType->print(smack::dbgs(), true)); + SDEBUG(FormalType->print(smack::dbgs(), true)); break; } } @@ -199,10 +199,10 @@ bool ArgCast::runOnModule(Module& M) { // Debug printing SDEBUG(errs() << "ARGCAST:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(CI->dump()); + SDEBUG(CI->print(smack::dbgs(), true)); SDEBUG(errs() << "ARGCAST:"); SDEBUG(errs() << "ADDED:"); - SDEBUG(CINew->dump()); + SDEBUG(CINew->print(smack::dbgs(), true)); CI->eraseFromParent(); numChanged++; diff --git a/lib/AssistDS/DSNodeEquivs.cpp b/lib/AssistDS/DSNodeEquivs.cpp index 318ab46da..8a9052ea5 100644 --- a/lib/AssistDS/DSNodeEquivs.cpp +++ b/lib/AssistDS/DSNodeEquivs.cpp @@ -116,7 +116,7 @@ FunctionList DSNodeEquivs::getCallees(CallSite &CS) { SDEBUG( if (Callees.empty()) { errs() << "Failed to get callees for callsite:\n"; - CS.getInstruction()->dump(); + CS.getInstruction()->print(smack::dbgs(), true); }); return Callees; diff --git a/lib/AssistDS/SimplifyExtractValue.cpp b/lib/AssistDS/SimplifyExtractValue.cpp index bdbabc897..e645fae6f 100644 --- a/lib/AssistDS/SimplifyExtractValue.cpp +++ b/lib/AssistDS/SimplifyExtractValue.cpp @@ -65,7 +65,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(Agg); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; @@ -76,7 +76,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(UndefValue::get(EV->getType())); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; @@ -86,7 +86,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(Constant::getNullValue(EV->getType())); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; @@ -104,7 +104,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(EV_new); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; @@ -113,7 +113,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(V); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; @@ -165,7 +165,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(EV_new); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; done = true; @@ -183,7 +183,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(IV->getInsertedValueOperand()); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; @@ -205,7 +205,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(NewIV); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; @@ -225,7 +225,7 @@ bool SimplifyEV::runOnModule(Module& M) { EV->replaceAllUsesWith(EV_new); SDEBUG(errs() << "EV:"); SDEBUG(errs() << "ERASE:"); - SDEBUG(EV->dump()); + SDEBUG(EV->print(smack::dbgs(), true)); EV->eraseFromParent(); numErased++; changed = true; diff --git a/lib/DSA/CallTargets.cpp b/lib/DSA/CallTargets.cpp index 55e8dd784..4fa9fc477 100644 --- a/lib/DSA/CallTargets.cpp +++ b/lib/DSA/CallTargets.cpp @@ -146,7 +146,7 @@ void CallTargetFinder::print(llvm::raw_ostream &O, const Module *M) const if (!isComplete(ii->first)) { O << "* "; CallSite cs = ii->first; - cs.getInstruction()->dump(); + cs.getInstruction()->print(O, true); O << cs.getInstruction()->getParent()->getParent()->getName().str() << " " << cs.getInstruction()->getName().str() << " "; } diff --git a/lib/DSA/DataStructure.cpp b/lib/DSA/DataStructure.cpp index fbed5ad76..60676135e 100644 --- a/lib/DSA/DataStructure.cpp +++ b/lib/DSA/DataStructure.cpp @@ -277,7 +277,7 @@ void DSNode::addValueList(std::vector &List) const { DSScalarMap &SN = getParentGraph()->getScalarMap(); for(DSScalarMap::const_iterator I = SN.begin(), E = SN.end(); I!= E; I++) { if(SN[I->first].getNode() == this){ - //I->first->dump(); + //I->first->print(smack::dbgs(), true); } } From d448e33f84960f1427401f62ec873babc3df1e68 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Tue, 16 Jul 2019 13:47:43 -0600 Subject: [PATCH 12/20] Reverted ToolOutputFile back to tool_output_file --- tools/llvm2bpl/llvm2bpl.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp index deec47534..f3f165c44 100644 --- a/tools/llvm2bpl/llvm2bpl.cpp +++ b/tools/llvm2bpl/llvm2bpl.cpp @@ -209,11 +209,11 @@ int main(int argc, char **argv) { pass_manager.add(new smack::AddTiming()); } - std::vector files; + std::vector files; if (!FinalIrFilename.empty()) { std::error_code EC; - auto F = new ToolOutputFile(FinalIrFilename.c_str(), EC, sys::fs::F_None); + auto F = new tool_output_file(FinalIrFilename.c_str(), EC, sys::fs::F_None); if (EC) check(EC.message()); F->keep(); @@ -223,7 +223,7 @@ int main(int argc, char **argv) { if (!OutputFilename.empty()) { std::error_code EC; - auto F = new ToolOutputFile(OutputFilename.c_str(), EC, sys::fs::F_None); + auto F = new tool_output_file(OutputFilename.c_str(), EC, sys::fs::F_None); if (EC) check(EC.message()); F->keep(); From 8a50446ab5062f776af76475e830735c27621a11 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Wed, 17 Jul 2019 12:40:41 -0600 Subject: [PATCH 13/20] Updated LLVM version in the installation documentation --- docs/installation.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/installation.md b/docs/installation.md index 0c26b62ea..f11c0cc9e 100644 --- a/docs/installation.md +++ b/docs/installation.md @@ -80,8 +80,8 @@ to Docker's official documentation. SMACK depends on the following projects: -* [LLVM][] version [4.0.1][LLVM-4.0.1] -* [Clang][] version [4.0.1][Clang-4.0.1] +* [LLVM][] version [5.0.2][LLVM-5.0.2] +* [Clang][] version [5.0.2][Clang-5.0.2] * [Python][] version 2.7 or greater * [Ninja][] version 1.5.1 or greater * [Mono][] version 5.0.0 or greater (except on Windows) @@ -203,9 +203,9 @@ shell in the `test` directory by executing [CMake]: http://www.cmake.org [Python]: http://www.python.org [LLVM]: http://llvm.org -[LLVM-4.0.1]: http://llvm.org/releases/download.html#4.0.1 +[LLVM-5.0.2]: http://llvm.org/releases/download.html#5.0.2 [Clang]: http://clang.llvm.org -[Clang-4.0.1]: http://llvm.org/releases/download.html#4.0.1 +[Clang-5.0.2]: http://llvm.org/releases/download.html#5.0.2 [Boogie]: https://github.com/boogie-org/boogie [Corral]: https://github.com/boogie-org/corral [Z3]: https://github.com/Z3Prover/z3/ From 90daca0e4605836b54332da6ab5323161921de76 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Wed, 17 Jul 2019 14:18:33 -0600 Subject: [PATCH 14/20] Disable the `optnone` attribute Otherwise the optimization passes SMACK employs do not get invoked. --- share/smack/frontend.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/share/smack/frontend.py b/share/smack/frontend.py index 8be250ac1..9927fae10 100644 --- a/share/smack/frontend.py +++ b/share/smack/frontend.py @@ -68,6 +68,10 @@ def smack_lib(): def default_clang_compile_command(args, lib = False): cmd = ['clang', '-c', '-emit-llvm', '-O0', '-g', '-gcolumn-info'] + # Starting from LLVM 5.0, we need the following two options + # in order to enable optimization passes. + # See: https://stackoverflow.com/a/46753969. + cmd += ['-Xclang', '-disable-O0-optnone'] cmd += map(lambda path: '-I' + path, smack_headers(args)) cmd += args.clang_options.split() cmd += ['-DMEMORY_MODEL_' + args.mem_mod.upper().replace('-','_')] From 0b1fdf9a14a28e948f16237ba1e505c32fac69d7 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Wed, 17 Jul 2019 15:54:00 -0600 Subject: [PATCH 15/20] Updated the LLVM version in CI (from 4.0 to 5.0) --- .travis.yml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/.travis.yml b/.travis.yml index 4ee4417b5..50d7ba52f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,7 +39,7 @@ env: before_install: - sudo rm -rf /usr/local/clang-7.0.0 - - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-4.0 main" + - sudo add-apt-repository "deb http://apt.llvm.org/xenial/ llvm-toolchain-xenial-5.0 main" - wget -O - http://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add - - sudo apt-key adv --keyserver hkp://keyserver.ubuntu.com:80 --recv-keys 3FA7E0328081BFF6A14DA29AA6A19B38D3D831EF - sudo apt-get install -y apt-transport-https @@ -47,13 +47,13 @@ before_install: - sudo apt-get update install: - - sudo apt-get install -y clang-4.0 clang-format-4.0 llvm-4.0-dev mono-complete ninja-build - - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-4.0 20 - - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-4.0 20 - - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-4.0 20 - - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-4.0 20 - - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-4.0 20 - - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-4.0 20 + - sudo apt-get install -y clang-5.0 clang-format-5.0 llvm-5.0-dev mono-complete ninja-build + - sudo update-alternatives --install /usr/bin/clang clang /usr/bin/clang-5.0 20 + - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-5.0 20 + - sudo update-alternatives --install /usr/bin/llvm-config llvm-config /usr/bin/llvm-config-5.0 20 + - sudo update-alternatives --install /usr/bin/llvm-link llvm-link /usr/bin/llvm-link-5.0 20 + - sudo update-alternatives --install /usr/bin/llvm-dis llvm-dis /usr/bin/llvm-dis-5.0 20 + - sudo update-alternatives --install /usr/bin/clang-format clang-format /usr/bin/clang-format-5.0 20 - sudo pip install pyyaml psutil script: From 1ba4273aee9ae3bf3fad19e7b94ec605d7db9d10 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Thu, 18 Jul 2019 01:36:23 -0600 Subject: [PATCH 16/20] Fixed formatting since we updated clang-format --- include/smack/BoogieAst.h | 2 +- include/smack/BplFilePrinter.h | 2 +- include/smack/BplPrinter.h | 2 +- include/smack/CodifyStaticInits.h | 2 +- include/smack/Contracts.h | 2 +- include/smack/DSAWrapper.h | 4 +- include/smack/ExtractContracts.h | 2 +- include/smack/IntegerOverflowChecker.h | 2 +- include/smack/MemorySafetyChecker.h | 2 +- include/smack/Naming.h | 2 +- include/smack/NormalizeLoops.h | 2 +- include/smack/Prelude.h | 2 +- include/smack/Regions.h | 2 +- include/smack/RemoveDeadDefs.h | 2 +- include/smack/SimplifyLibCalls.h | 2 +- include/smack/Slicing.h | 2 +- include/smack/SmackInstGenerator.h | 2 +- include/smack/SmackModuleGenerator.h | 2 +- include/smack/SmackOptions.h | 2 +- include/smack/SmackRep.h | 2 +- include/smack/SmackWarnings.h | 2 +- include/smack/SplitAggregateValue.h | 2 +- include/smack/VectorOperations.h | 2 +- include/smack/VerifierCodeMetadata.h | 2 +- lib/smack/BoogieAst.cpp | 2 +- lib/smack/BplFilePrinter.cpp | 2 +- lib/smack/BplPrinter.cpp | 2 +- lib/smack/CodifyStaticInits.cpp | 6 +- lib/smack/Contracts.cpp | 2 +- lib/smack/Debug.cpp | 11 +- lib/smack/ExtractContracts.cpp | 4 +- lib/smack/IntegerOverflowChecker.cpp | 2 +- lib/smack/MemorySafetyChecker.cpp | 4 +- lib/smack/Naming.cpp | 2 +- lib/smack/NormalizeLoops.cpp | 2 +- lib/smack/Prelude.cpp | 40 +++--- lib/smack/Regions.cpp | 4 +- lib/smack/RemoveDeadDefs.cpp | 2 +- lib/smack/SimplifyLibCalls.cpp | 2 +- lib/smack/Slicing.cpp | 2 +- lib/smack/SmackInstGenerator.cpp | 59 ++++---- lib/smack/SmackOptions.cpp | 2 +- lib/smack/SmackRep.cpp | 37 ++--- lib/smack/SmackWarnings.cpp | 2 +- lib/smack/SplitAggregateValue.cpp | 2 +- lib/smack/VectorOperations.cpp | 14 +- lib/smack/VerifierCodeMetadata.cpp | 4 +- share/smack/include/pthreadtypes.h | 8 +- share/smack/include/smack.h | 4 +- test/contracts/failing/array_forall.c | 10 +- test/contracts/failing/array_forall_fail.c | 10 +- test/contracts/failing/forall.c | 4 +- test/contracts/failing/forall_fail.c | 5 +- test/data/struct_cast.c | 4 +- test/data/struct_cast1.c | 4 +- test/data/struct_cast1_fail.c | 4 +- test/data/struct_cast_fail.c | 4 +- test/ntdrivers/cdaudio_true.i.cil.c | 2 +- test/ntdrivers/floppy2_true.i.cil.c | 74 +++++----- test/ntdrivers/floppy_false.i.cil.c | 159 +++++++++++---------- test/ntdrivers/floppy_true.i.cil.c | 159 +++++++++++---------- test/ntdrivers/parport_false.i.cil.c | 37 +++-- test/ntdrivers/parport_true.i.cil.c | 37 +++-- 63 files changed, 399 insertions(+), 385 deletions(-) diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h index 34ff1230b..aa3c6b0aa 100644 --- a/include/smack/BoogieAst.h +++ b/include/smack/BoogieAst.h @@ -680,6 +680,6 @@ std::ostream &operator<<(std::ostream &os, const Expr *e); std::ostream &operator<<(std::ostream &os, Decl &e); std::ostream &operator<<(std::ostream &os, Decl *e); -} +} // namespace smack #endif // BOOGIEAST_H diff --git a/include/smack/BplFilePrinter.h b/include/smack/BplFilePrinter.h index abb9e46a1..eb339c5ae 100644 --- a/include/smack/BplFilePrinter.h +++ b/include/smack/BplFilePrinter.h @@ -23,6 +23,6 @@ class BplFilePrinter : public llvm::ModulePass { virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const; }; -} +} // namespace smack #endif // BPLPRINTER_H diff --git a/include/smack/BplPrinter.h b/include/smack/BplPrinter.h index 0f41ce40e..0c3f39c8e 100644 --- a/include/smack/BplPrinter.h +++ b/include/smack/BplPrinter.h @@ -17,6 +17,6 @@ class BplPrinter : public llvm::ModulePass { virtual bool runOnModule(llvm::Module &m); virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const; }; -} +} // namespace smack #endif // BPLPRINTER_H diff --git a/include/smack/CodifyStaticInits.h b/include/smack/CodifyStaticInits.h index 36fb1307b..8a30c48dc 100644 --- a/include/smack/CodifyStaticInits.h +++ b/include/smack/CodifyStaticInits.h @@ -20,4 +20,4 @@ class CodifyStaticInits : public llvm::ModulePass { virtual bool runOnModule(llvm::Module &M); virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const; }; -} +} // namespace smack diff --git a/include/smack/Contracts.h b/include/smack/Contracts.h index 7a8365163..0f7f85c69 100644 --- a/include/smack/Contracts.h +++ b/include/smack/Contracts.h @@ -33,4 +33,4 @@ class ContractsExtractor : public InstVisitor { return ConstantInt::get(Type::getInt32Ty(ctx), slices.size()); } }; -} +} // namespace smack diff --git a/include/smack/DSAWrapper.h b/include/smack/DSAWrapper.h index 954e3328d..ef009069d 100644 --- a/include/smack/DSAWrapper.h +++ b/include/smack/DSAWrapper.h @@ -17,7 +17,7 @@ class DSGraph; class TDDataStructures; class BUDataStructures; class DSNodeEquivs; -} +} // namespace llvm namespace dsa { template struct TypeSafety; @@ -74,6 +74,6 @@ class DSAWrapper : public llvm::ModulePass { const llvm::DSNode *getNode(const llvm::Value *v); void printDSAGraphs(const char *Filename); }; -} +} // namespace smack #endif // DSAWRAPPER_H diff --git a/include/smack/ExtractContracts.h b/include/smack/ExtractContracts.h index 4fbcf6d95..bbd385826 100644 --- a/include/smack/ExtractContracts.h +++ b/include/smack/ExtractContracts.h @@ -16,4 +16,4 @@ class ExtractContracts : public ModulePass { virtual bool runOnModule(Module &M); virtual void getAnalysisUsage(AnalysisUsage &AU) const; }; -} +} // namespace smack diff --git a/include/smack/IntegerOverflowChecker.h b/include/smack/IntegerOverflowChecker.h index ebace5fcc..a21f63d34 100644 --- a/include/smack/IntegerOverflowChecker.h +++ b/include/smack/IntegerOverflowChecker.h @@ -32,6 +32,6 @@ class IntegerOverflowChecker : public llvm::ModulePass { void addBlockingAssume(llvm::Function *va, llvm::Value *flag, llvm::Instruction *i); }; -} +} // namespace smack #endif // INTEGEROVERFLOWCHECKER_H diff --git a/include/smack/MemorySafetyChecker.h b/include/smack/MemorySafetyChecker.h index e8d76be5b..f692a80ad 100644 --- a/include/smack/MemorySafetyChecker.h +++ b/include/smack/MemorySafetyChecker.h @@ -35,6 +35,6 @@ class MemorySafetyChecker : public llvm::FunctionPass, void visitMemSetInst(llvm::MemSetInst &I); void visitMemTransferInst(llvm::MemTransferInst &I); }; -} +} // namespace smack #endif // MEMORYSAFETYCHECKER_H diff --git a/include/smack/Naming.h b/include/smack/Naming.h index cd7437c01..c41fa7103 100644 --- a/include/smack/Naming.h +++ b/include/smack/Naming.h @@ -116,6 +116,6 @@ class Naming { static bool isSmackGeneratedName(std::string s); static std::string escape(std::string s); }; -} +} // namespace smack #endif diff --git a/include/smack/NormalizeLoops.h b/include/smack/NormalizeLoops.h index c1594d37e..f43a7f3fa 100644 --- a/include/smack/NormalizeLoops.h +++ b/include/smack/NormalizeLoops.h @@ -19,6 +19,6 @@ class NormalizeLoops : public llvm::ModulePass { virtual bool runOnModule(llvm::Module &m) override; virtual void getAnalysisUsage(llvm::AnalysisUsage &) const override; }; -} +} // namespace smack #endif // NORMALIZELOOPS_H diff --git a/include/smack/Prelude.h b/include/smack/Prelude.h index de4fb313d..7c8daf677 100644 --- a/include/smack/Prelude.h +++ b/include/smack/Prelude.h @@ -215,6 +215,6 @@ class Prelude { FuncDecl *unsafeStore(Binding elemBinding, const Expr *body, bool bytes = true); }; -} +} // namespace smack #endif // PRELUDE_H diff --git a/include/smack/Regions.h b/include/smack/Regions.h index 0f89aef4d..a5b903107 100644 --- a/include/smack/Regions.h +++ b/include/smack/Regions.h @@ -92,6 +92,6 @@ class Regions : public ModulePass, public InstVisitor { void visitMemIntrinsic(MemIntrinsic &); void visitCallInst(CallInst &); }; -} +} // namespace smack #endif // REGIONS_H diff --git a/include/smack/RemoveDeadDefs.h b/include/smack/RemoveDeadDefs.h index eb18c5fdb..708832f10 100644 --- a/include/smack/RemoveDeadDefs.h +++ b/include/smack/RemoveDeadDefs.h @@ -18,4 +18,4 @@ class RemoveDeadDefs : public llvm::ModulePass { RemoveDeadDefs() : llvm::ModulePass(ID) {} virtual bool runOnModule(llvm::Module &M); }; -} +} // namespace smack diff --git a/include/smack/SimplifyLibCalls.h b/include/smack/SimplifyLibCalls.h index 05f72d394..227f7eed3 100644 --- a/include/smack/SimplifyLibCalls.h +++ b/include/smack/SimplifyLibCalls.h @@ -25,4 +25,4 @@ class SimplifyLibCalls : public ModulePass, virtual bool runOnModule(Module &M); void visitCallInst(CallInst &); }; -} +} // namespace smack diff --git a/include/smack/Slicing.h b/include/smack/Slicing.h index de9016e60..e5659e791 100644 --- a/include/smack/Slicing.h +++ b/include/smack/Slicing.h @@ -40,6 +40,6 @@ class Slice { const Decl *getBoogieDecl(Naming *naming, SmackRep *rep); const Expr *getBoogieExpression(Naming *naming, SmackRep *rep); }; -} +} // namespace smack #endif diff --git a/include/smack/SmackInstGenerator.h b/include/smack/SmackInstGenerator.h index 604b9ed49..18f897b7f 100644 --- a/include/smack/SmackInstGenerator.h +++ b/include/smack/SmackInstGenerator.h @@ -98,6 +98,6 @@ class SmackInstGenerator : public llvm::InstVisitor { void visitMemSetInst(llvm::MemSetInst &i); void visitIntrinsicInst(llvm::IntrinsicInst &i); }; -} +} // namespace smack #endif // SMACKINSTVISITOR_H diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h index 3735fd88e..dcfb4df07 100644 --- a/include/smack/SmackModuleGenerator.h +++ b/include/smack/SmackModuleGenerator.h @@ -23,6 +23,6 @@ class SmackModuleGenerator : public llvm::ModulePass { void generateProgram(llvm::Module &m); Program *getProgram() { return program; } }; -} +} // namespace smack #endif // SMACKMODULEGENERATOR_H diff --git a/include/smack/SmackOptions.h b/include/smack/SmackOptions.h index 3c27642d8..66c0f34dc 100644 --- a/include/smack/SmackOptions.h +++ b/include/smack/SmackOptions.h @@ -32,6 +32,6 @@ class SmackOptions { static bool isEntryPoint(std::string); }; -} +} // namespace smack #endif // SMACKREP_H diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h index ed3ca92a6..2604150e4 100644 --- a/include/smack/SmackRep.h +++ b/include/smack/SmackRep.h @@ -197,6 +197,6 @@ class SmackRep { std::string opName(const std::string &operation, std::list types); }; -} +} // namespace smack #endif // SMACKREP_H diff --git a/include/smack/SmackWarnings.h b/include/smack/SmackWarnings.h index f271759e1..3713f925d 100644 --- a/include/smack/SmackWarnings.h +++ b/include/smack/SmackWarnings.h @@ -50,6 +50,6 @@ class SmackWarnings { static bool isSufficientWarningLevel(WarningLevel level); static std::string getFlagStr(UnsetFlagsT flags); }; -} +} // namespace smack #endif // SMACKWARNINGS_H diff --git a/include/smack/SplitAggregateValue.h b/include/smack/SplitAggregateValue.h index ccaccb1fe..98a06362a 100644 --- a/include/smack/SplitAggregateValue.h +++ b/include/smack/SplitAggregateValue.h @@ -36,4 +36,4 @@ class SplitAggregateValue : public llvm::BasicBlockPass { std::vector &info, llvm::Value *V); bool isConstantAggregate(llvm::Value *V); }; -} +} // namespace smack diff --git a/include/smack/VectorOperations.h b/include/smack/VectorOperations.h index 740cc87c5..b277e5f8e 100644 --- a/include/smack/VectorOperations.h +++ b/include/smack/VectorOperations.h @@ -41,6 +41,6 @@ class VectorOperations { FuncDecl *load(const Value *V); FuncDecl *store(const Value *V); }; -} +} // namespace smack #endif // VECTOROPERATIONS_H diff --git a/include/smack/VerifierCodeMetadata.h b/include/smack/VerifierCodeMetadata.h index 59352fb5f..dd91a56fe 100644 --- a/include/smack/VerifierCodeMetadata.h +++ b/include/smack/VerifierCodeMetadata.h @@ -26,4 +26,4 @@ class VerifierCodeMetadata : public ModulePass, void visitInstruction(Instruction &); static bool isMarked(const Instruction &I); }; -} +} // namespace smack diff --git a/lib/smack/BoogieAst.cpp b/lib/smack/BoogieAst.cpp index 13035999e..aa1061d57 100644 --- a/lib/smack/BoogieAst.cpp +++ b/lib/smack/BoogieAst.cpp @@ -685,4 +685,4 @@ void Program::print(std::ostream &os) const { print_seq(os, decls, "\n"); os << "\n"; } -} +} // namespace smack diff --git a/lib/smack/BplFilePrinter.cpp b/lib/smack/BplFilePrinter.cpp index 414e16f6e..89db68464 100644 --- a/lib/smack/BplFilePrinter.cpp +++ b/lib/smack/BplFilePrinter.cpp @@ -28,4 +28,4 @@ bool BplFilePrinter::runOnModule(llvm::Module &m) { // DEBUG_WITH_TYPE("bpl", errs() << "" << s.str()); return false; } -} +} // namespace smack diff --git a/lib/smack/BplPrinter.cpp b/lib/smack/BplPrinter.cpp index 2e1baf5c1..11c130cbf 100644 --- a/lib/smack/BplPrinter.cpp +++ b/lib/smack/BplPrinter.cpp @@ -28,4 +28,4 @@ bool BplPrinter::runOnModule(llvm::Module &m) { DEBUG_WITH_TYPE("bpl", errs() << "" << s.str()); return false; } -} +} // namespace smack diff --git a/lib/smack/CodifyStaticInits.cpp b/lib/smack/CodifyStaticInits.cpp index 3db86b593..406e3de44 100644 --- a/lib/smack/CodifyStaticInits.cpp +++ b/lib/smack/CodifyStaticInits.cpp @@ -28,8 +28,8 @@ bool CodifyStaticInits::runOnModule(Module &M) { LLVMContext &C = M.getContext(); DSAWrapper *DSA = &getAnalysis(); - Function *F = dyn_cast(M.getOrInsertFunction( - Naming::STATIC_INIT_PROC, Type::getVoidTy(C))); + Function *F = dyn_cast( + M.getOrInsertFunction(Naming::STATIC_INIT_PROC, Type::getVoidTy(C))); BasicBlock *B = BasicBlock::Create(C, "entry", F); IRBuilder<> IRB(B); @@ -101,4 +101,4 @@ char CodifyStaticInits::ID = 0; // Register the pass static RegisterPass X("codify-static-inits", "Codify Static Initializers"); -} +} // namespace smack diff --git a/lib/smack/Contracts.cpp b/lib/smack/Contracts.cpp index 6c8d850e3..9db27fba3 100644 --- a/lib/smack/Contracts.cpp +++ b/lib/smack/Contracts.cpp @@ -93,4 +93,4 @@ void ContractsExtractor::visitCallInst(CallInst &ci) { head->getInstList().insert(I, &ci); } } -} +} // namespace smack diff --git a/lib/smack/Debug.cpp b/lib/smack/Debug.cpp index 9b7668786..1d12f49bd 100644 --- a/lib/smack/Debug.cpp +++ b/lib/smack/Debug.cpp @@ -36,7 +36,7 @@ void setCurrentDebugTypes(const char **Types, unsigned Count) { for (size_t T = 0; T < Count; ++T) CurrentDebugType->push_back(Types[T]); } -} +} // namespace smack #ifndef NDEBUG @@ -57,13 +57,14 @@ struct DebugOnlyOpt { CurrentDebugType->push_back(dbgType); } }; -} +} // namespace static DebugOnlyOpt DebugOnlyOptLoc; static ::llvm::cl::opt> - DebugOnly("debug-only", cl::desc("Enable a specific type of debug output " - "(comma separated list of types)"), + DebugOnly("debug-only", + cl::desc("Enable a specific type of debug output " + "(comma separated list of types)"), cl::Hidden, cl::ZeroOrMore, cl::value_desc("debug string"), cl::location(DebugOnlyOptLoc), cl::ValueRequired); @@ -80,6 +81,6 @@ raw_ostream &smack::dbgs() { #else namespace smack { raw_ostream &dbgs() { return llvm::errs(); } -} +} // namespace smack #endif diff --git a/lib/smack/ExtractContracts.cpp b/lib/smack/ExtractContracts.cpp index 39f34dd10..f0cc0b00c 100644 --- a/lib/smack/ExtractContracts.cpp +++ b/lib/smack/ExtractContracts.cpp @@ -204,7 +204,7 @@ std::vector> getContractExprs(Function &F) { } return Fs; } -} +} // namespace bool ExtractContracts::runOnModule(Module &M) { bool modified = false; @@ -303,4 +303,4 @@ char ExtractContracts::ID = 0; // Register the pass static RegisterPass X("extract-contracts", "Extract Contracts"); -} +} // namespace smack diff --git a/lib/smack/IntegerOverflowChecker.cpp b/lib/smack/IntegerOverflowChecker.cpp index be6eaf7a8..848e95b60 100644 --- a/lib/smack/IntegerOverflowChecker.cpp +++ b/lib/smack/IntegerOverflowChecker.cpp @@ -222,4 +222,4 @@ char IntegerOverflowChecker::ID = 0; StringRef IntegerOverflowChecker::getPassName() const { return "Checked integer arithmetic intrinsics"; } -} +} // namespace smack diff --git a/lib/smack/MemorySafetyChecker.cpp b/lib/smack/MemorySafetyChecker.cpp index e37c39905..ca88afa90 100644 --- a/lib/smack/MemorySafetyChecker.cpp +++ b/lib/smack/MemorySafetyChecker.cpp @@ -92,7 +92,7 @@ Value *accessSizeAsPointer(StoreInst &I) { auto &M = *I.getParent()->getParent()->getParent(); return accessSizeAsPointer(M, I.getPointerOperand()); } -} +} // namespace void MemorySafetyChecker::visitLoadInst(LoadInst &I) { insertMemoryAccessCheck(I.getPointerOperand(), accessSizeAsPointer(I), &I); @@ -113,4 +113,4 @@ void MemorySafetyChecker::visitMemTransferInst(MemTransferInst &I) { // Pass ID variable char MemorySafetyChecker::ID = 0; -} +} // namespace smack diff --git a/lib/smack/Naming.cpp b/lib/smack/Naming.cpp index b999d7f26..3317263e9 100644 --- a/lib/smack/Naming.cpp +++ b/lib/smack/Naming.cpp @@ -267,4 +267,4 @@ std::string Naming::freshVarName(const Value &V) { s << varNum++; return s.str(); } -} +} // namespace smack diff --git a/lib/smack/NormalizeLoops.cpp b/lib/smack/NormalizeLoops.cpp index 156e39fe3..d21a5f1a5 100644 --- a/lib/smack/NormalizeLoops.cpp +++ b/lib/smack/NormalizeLoops.cpp @@ -158,4 +158,4 @@ bool NormalizeLoops::runOnModule(Module &m) { char NormalizeLoops::ID = 0; StringRef NormalizeLoops::getPassName() const { return "NormalizeLoops"; } -} +} // namespace smack diff --git a/lib/smack/Prelude.cpp b/lib/smack/Prelude.cpp index c48ad0c3e..6cb920185 100644 --- a/lib/smack/Prelude.cpp +++ b/lib/smack/Prelude.cpp @@ -367,14 +367,17 @@ void IntOpGen::generateArithOps(std::stringstream &s) const { const auto intBuiltinOp = new BuiltinOp(IntOp::intAttrFunc); const auto uninterpretedOp = new UninterpretedOp(); const std::vector intArithOpTable{ - {"add", 2, new InlinedOp( - IntOpGen::IntArithOp::intArithExpr), + {"add", 2, + new InlinedOp( + IntOpGen::IntArithOp::intArithExpr), bvBuiltinOp, true}, - {"sub", 2, new InlinedOp( - IntOpGen::IntArithOp::intArithExpr), + {"sub", 2, + new InlinedOp( + IntOpGen::IntArithOp::intArithExpr), bvBuiltinOp, true}, - {"mul", 2, new InlinedOp( - IntOpGen::IntArithOp::intArithExpr), + {"mul", 2, + new InlinedOp( + IntOpGen::IntArithOp::intArithExpr), bvBuiltinOp, true}, {"sdiv", 2, intBuiltinOp, bvBuiltinOp, false}, {"smod", 2, intBuiltinOp, bvBuiltinOp, false}, @@ -874,9 +877,9 @@ void MemDeclGen::generateGlobalAllocations(std::stringstream &s) const { std::list stmts; for (auto E : prelude.rep.globalAllocations) - stmts.push_back(Stmt::call( - "$galloc", - {prelude.rep.expr(E.first), prelude.rep.pointerLit(E.second)})); + stmts.push_back( + Stmt::call("$galloc", {prelude.rep.expr(E.first), + prelude.rep.pointerLit(E.second)})); s << Decl::procedure("$global_allocations", {}, {}, {}, {Block::block("", stmts)}) << "\n"; @@ -924,9 +927,8 @@ void PtrOpGen::generatePreds(std::stringstream &s) const { indexedName(pred, {Naming::PTR_TYPE}), {{"p1", Naming::PTR_TYPE}, {"p2", Naming::PTR_TYPE}}, prelude.rep.intType(1), - Expr::cond(Expr::fn(indexedName(pred, - {prelude.rep.pointerType(), - Naming::BOOL_TYPE}), + Expr::cond(Expr::fn(indexedName(pred, {prelude.rep.pointerType(), + Naming::BOOL_TYPE}), {Expr::id("p1"), Expr::id("p2")}), prelude.rep.integerLit(1LL, 1), prelude.rep.integerLit(0LL, 1)), @@ -1449,9 +1451,10 @@ void FpOpGen::generateMemOps(std::stringstream &s) const { // e.g., function {:inline} $load.unsafe.bvhalf(M: [ref] i8, p: ref) // returns (bvhalf) { $bitcast.i16.bvhalf($load.i16(M, p)) } s << prelude.unsafeLoad( - type, Expr::fn(indexedName("$bitcast", {intType, type}), - Expr::fn(indexedName("$load", {intType}), - makeMapVarExpr(0), makePtrVarExpr(0))), + type, + Expr::fn(indexedName("$bitcast", {intType, type}), + Expr::fn(indexedName("$load", {intType}), + makeMapVarExpr(0), makePtrVarExpr(0))), false) << "\n"; // e.g., function {:inline} $store.unsafe.bvfloat(M: [ref] i8, p: ref, @@ -1488,10 +1491,9 @@ void FpOpGen::generateMemOps(std::stringstream &s) const { // function {:inline} $store.bytes.float(M: [ref] bv8, p: ref, f: float) // returns ([ref] bv8) { M[p := $bitcast.float.bv8(f)] } s << prelude.unsafeStore( - binding, - prelude.mapUpdExpr( - 0, Expr::fn(indexedName("$bitcast", {type, bvType}), - makeFpVarExpr(0)))) + binding, prelude.mapUpdExpr( + 0, Expr::fn(indexedName("$bitcast", {type, bvType}), + makeFpVarExpr(0)))) << "\n"; } else { std::string intType = getIntTypeName(8); diff --git a/lib/smack/Regions.cpp b/lib/smack/Regions.cpp index c1d20e3e2..5b746df56 100644 --- a/lib/smack/Regions.cpp +++ b/lib/smack/Regions.cpp @@ -42,7 +42,7 @@ bool isFieldDisjoint(DSAWrapper *DSA, const Value *V, unsigned offset) { else return DSA->isFieldDisjoint(V, getFunction(V)); } -} +} // namespace void Region::init(Module &M, Pass &P) { DL = &M.getDataLayout(); @@ -75,7 +75,7 @@ unsigned numGlobals(const DSNode *N) { return count; } -} +} // namespace bool Region::isSingleton(const DSNode *N, unsigned offset, unsigned length) { if (N->isGlobalNode() && numGlobals(N) == 1 && !N->isArrayNode() && diff --git a/lib/smack/RemoveDeadDefs.cpp b/lib/smack/RemoveDeadDefs.cpp index 09d1a9aa7..0caecdaea 100644 --- a/lib/smack/RemoveDeadDefs.cpp +++ b/lib/smack/RemoveDeadDefs.cpp @@ -54,4 +54,4 @@ char RemoveDeadDefs::ID = 0; // Register the pass static RegisterPass X("remove-dead-defs", "Remove Dead Definitions"); -} +} // namespace smack diff --git a/lib/smack/SimplifyLibCalls.cpp b/lib/smack/SimplifyLibCalls.cpp index 6c65cae8a..f4dd57f5d 100644 --- a/lib/smack/SimplifyLibCalls.cpp +++ b/lib/smack/SimplifyLibCalls.cpp @@ -46,4 +46,4 @@ char SimplifyLibCalls::ID = 0; // Register the pass static RegisterPass X("simplify-libcalls", "Simplify Library Calls"); -} +} // namespace smack diff --git a/lib/smack/Slicing.cpp b/lib/smack/Slicing.cpp index 4e4f57234..d20f08f27 100644 --- a/lib/smack/Slicing.cpp +++ b/lib/smack/Slicing.cpp @@ -271,4 +271,4 @@ const Expr *Slice::getBoogieExpression(Naming &naming, SmackRep &rep) { args.push_back(Expr::id(getParameter(*V, naming, rep).first)); return Expr::fn(getName(), args); } -} +} // namespace smack diff --git a/lib/smack/SmackInstGenerator.cpp b/lib/smack/SmackInstGenerator.cpp index d9133972f..94d6e2eaa 100644 --- a/lib/smack/SmackInstGenerator.cpp +++ b/lib/smack/SmackInstGenerator.cpp @@ -164,10 +164,9 @@ void SmackInstGenerator::visitBasicBlock(llvm::BasicBlock &bb) { emit(recordProcedureCall( F, {Attr::attr("cexpr", "smack:entry:" + naming->get(*F))})); for (auto &A : F->args()) { - emit(recordProcedureCall(&A, - {Attr::attr("cexpr", - "smack:arg:" + naming->get(*F) + - ":" + naming->get(A))})); + emit(recordProcedureCall( + &A, {Attr::attr("cexpr", "smack:arg:" + naming->get(*F) + ":" + + naming->get(A))})); } } } @@ -845,9 +844,8 @@ void SmackInstGenerator::visitDbgValueInst(llvm::DbgValueInst &dvi) { for (auto &arg : F->args()) { if (&arg == V && var->getScope() == F->getMetadata("dbg")) { emit(recordProcedureCall( - V, - {Attr::attr("cexpr", - naming->get(*F) + ":arg:" + var->getName().str())})); + V, {Attr::attr("cexpr", naming->get(*F) + + ":arg:" + var->getName().str())})); break; } } @@ -890,21 +888,21 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) { processInstruction(ii); //(CallInst -> Void) -> [Flags] -> (CallInst -> Void) - static const auto conditionalModel = [this]( - std::function modelGenFunc, - std::initializer_list *> requiredFlags) { - auto unsetFlags = SmackWarnings::getUnsetFlags(requiredFlags); - return [this, unsetFlags, modelGenFunc](CallInst *ci) { - if (unsetFlags.empty()) - modelGenFunc(ci); - else { - SmackWarnings::warnUnsound("call to " + - ci->getCalledFunction()->getName().str(), - unsetFlags, currBlock, ci); - emit(rep->call(ci->getCalledFunction(), *ci)); - } - }; - }; + static const auto conditionalModel = + [this](std::function modelGenFunc, + std::initializer_list *> requiredFlags) { + auto unsetFlags = SmackWarnings::getUnsetFlags(requiredFlags); + return [this, unsetFlags, modelGenFunc](CallInst *ci) { + if (unsetFlags.empty()) + modelGenFunc(ci); + else { + SmackWarnings::warnUnsound( + "call to " + ci->getCalledFunction()->getName().str(), + unsetFlags, currBlock, ci); + emit(rep->call(ci->getCalledFunction(), *ci)); + } + }; + }; static const auto f16UpCast = conditionalModel( [this](CallInst *ci) { @@ -1067,14 +1065,15 @@ void SmackInstGenerator::visitIntrinsicInst(llvm::IntrinsicInst &ii) { return body; }; - static const auto assignBvExpr = [this]( - std::function exprGenFunc) { - return conditionalModel( - [this, exprGenFunc](CallInst *ci) { - emit(Stmt::assign(rep->expr(ci), exprGenFunc(ci->getArgOperand(0)))); - }, - {&SmackOptions::BitPrecise}); - }; + static const auto assignBvExpr = + [this](std::function exprGenFunc) { + return conditionalModel( + [this, exprGenFunc](CallInst *ci) { + emit(Stmt::assign(rep->expr(ci), + exprGenFunc(ci->getArgOperand(0)))); + }, + {&SmackOptions::BitPrecise}); + }; static const auto assignUnFPFuncApp = [this](std::string fnBase) { return conditionalModel( diff --git a/lib/smack/SmackOptions.cpp b/lib/smack/SmackOptions.cpp index 3a3c347df..6c835170c 100644 --- a/lib/smack/SmackOptions.cpp +++ b/lib/smack/SmackOptions.cpp @@ -72,4 +72,4 @@ bool SmackOptions::isEntryPoint(std::string name) { return true; return false; } -} +} // namespace smack diff --git a/lib/smack/SmackRep.cpp b/lib/smack/SmackRep.cpp index 0f3ee908a..6fbc645aa 100644 --- a/lib/smack/SmackRep.cpp +++ b/lib/smack/SmackRep.cpp @@ -48,7 +48,7 @@ std::list findCallers(Function *F) { return callers; } -} +} // namespace namespace smack { @@ -377,13 +377,14 @@ const Stmt *SmackRep::valueAnnotation(const CallInst &CI) { const unsigned R = regions->idx(GEP); bool bytewise = regions->get(R).bytewiseAccess(); attrs.push_back(Attr::attr("name", {Expr::id(naming->get(*A))})); - attrs.push_back( - Attr::attr("field", - { - Expr::lit(Naming::LOAD + "." + - (bytewise ? "bytes." : "") + intType(bits)), - Expr::id(memPath(R)), ptrArith(GEP), Expr::lit(bytes), - })); + attrs.push_back(Attr::attr( + "field", { + Expr::lit(Naming::LOAD + "." + + (bytewise ? "bytes." : "") + intType(bits)), + Expr::id(memPath(R)), + ptrArith(GEP), + Expr::lit(bytes), + })); } else { llvm_unreachable("Unexpected argument type."); @@ -512,9 +513,10 @@ const Expr *SmackRep::load(const llvm::Value *P) { const Expr *M = Expr::id(memPath(R)); std::string N = Naming::LOAD + "." + - (bytewise ? "bytes." : (isUnsafeFloatAccess(T->getElementType(), resultTy) - ? "unsafe." - : "")) + + (bytewise + ? "bytes." + : (isUnsafeFloatAccess(T->getElementType(), resultTy) ? "unsafe." + : "")) + type(T->getElementType()); return singleton ? M : Expr::fn(N, M, SmackRep::expr(P)); } @@ -547,8 +549,9 @@ const Expr *SmackRep::pa(const Expr *base, long long idx, unsigned size) { if (idx >= 0) { return pa(base, pointerLit(idx), pointerLit(size)); } else { - return pa(base, Expr::fn("$sub.ref", pointerLit(0ULL), - pointerLit((unsigned long long)std::abs(idx))), + return pa(base, + Expr::fn("$sub.ref", pointerLit(0ULL), + pointerLit((unsigned long long)std::abs(idx))), pointerLit(size)); } } @@ -772,8 +775,9 @@ const Expr *SmackRep::ptrArith( "Index value too large (or too small if negative)"); e = pa(e, (long long)ci->getSExtValue(), storageSize(et)); } else - e = pa(e, integerToPointer(expr(a.first), - a.first->getType()->getIntegerBitWidth()), + e = pa(e, + integerToPointer(expr(a.first), + a.first->getType()->getIntegerBitWidth()), storageSize(et)); } } @@ -1168,8 +1172,7 @@ unsigned SmackRep::numElements(const llvm::Constant *v) { void SmackRep::addInitFunc(const llvm::Function *f) { assert(f->getReturnType()->isVoidTy() && "Init functions cannot return a value"); - assert(f->arg_empty() && - "Init functions cannot take parameters"); + assert(f->arg_empty() && "Init functions cannot take parameters"); initFuncs.push_back(naming->get(*f)); } diff --git a/lib/smack/SmackWarnings.cpp b/lib/smack/SmackWarnings.cpp index a8408aec9..8746c10e3 100644 --- a/lib/smack/SmackWarnings.cpp +++ b/lib/smack/SmackWarnings.cpp @@ -95,4 +95,4 @@ void SmackWarnings::warnInfo(std::string info) { return; errs() << "warning: " << info << "\n"; } -} +} // namespace smack diff --git a/lib/smack/SplitAggregateValue.cpp b/lib/smack/SplitAggregateValue.cpp index 4aa57f3ba..bd9243901 100644 --- a/lib/smack/SplitAggregateValue.cpp +++ b/lib/smack/SplitAggregateValue.cpp @@ -170,4 +170,4 @@ char SplitAggregateValue::ID = 0; static RegisterPass X("split-aggregate-values", "Split Load/Store/ConstantReturn of Aggregate Types"); -} +} // namespace smack diff --git a/lib/smack/VectorOperations.cpp b/lib/smack/VectorOperations.cpp index 9a6c7e83f..96d090aad 100644 --- a/lib/smack/VectorOperations.cpp +++ b/lib/smack/VectorOperations.cpp @@ -97,9 +97,9 @@ FuncDecl *VectorOperations::binary(unsigned OpCode, VectorType *T) { rep->opName(Naming::INSTRUCTION_TABLE.at(OpCode), {T->getElementType()}); std::list Args; for (unsigned i = 0; i < T->getNumElements(); i++) { - Args.push_back(Expr::fn(FnBase, - {Expr::fn(selector(T, i), Expr::id("v1")), - Expr::fn(selector(T, i), Expr::id("v2"))})); + Args.push_back( + Expr::fn(FnBase, {Expr::fn(selector(T, i), Expr::id("v1")), + Expr::fn(selector(T, i), Expr::id("v2"))})); } return Decl::function(FnName, {{"v1", rep->type(T)}, {"v2", rep->type(T)}}, rep->type(T), Expr::fn(constructor(T), Args)); @@ -110,9 +110,9 @@ FuncDecl *VectorOperations::cmp(CmpInst::Predicate P, VectorType *T) { auto FnBase = rep->opName(Naming::CMPINST_TABLE.at(P), {T->getElementType()}); std::list Args; for (unsigned i = 0; i < T->getNumElements(); i++) { - Args.push_back(Expr::fn(FnBase, - {Expr::fn(selector(T, i), Expr::id("v1")), - Expr::fn(selector(T, i), Expr::id("v2"))})); + Args.push_back( + Expr::fn(FnBase, {Expr::fn(selector(T, i), Expr::id("v1")), + Expr::fn(selector(T, i), Expr::id("v2"))})); } return Decl::function( FnName, {{"v1", rep->type(T)}, {"v2", rep->type(T)}}, @@ -303,4 +303,4 @@ FuncDecl *VectorOperations::store(const Value *V) { rep->addAuxiliaryDeclaration(F); return F; } -} +} // namespace smack diff --git a/lib/smack/VerifierCodeMetadata.cpp b/lib/smack/VerifierCodeMetadata.cpp index 0b78761fe..5faee6a61 100644 --- a/lib/smack/VerifierCodeMetadata.cpp +++ b/lib/smack/VerifierCodeMetadata.cpp @@ -66,7 +66,7 @@ bool onlyVerifierUsers(Instruction &I) { } return true; } -} +} // namespace bool VerifierCodeMetadata::isMarked(const Instruction &I) { auto *N = I.getMetadata("verifier.code"); @@ -124,4 +124,4 @@ char VerifierCodeMetadata::ID = 0; // Register the pass static RegisterPass X("verifier-code-metadata", "Verifier Code Metadata"); -} +} // namespace smack diff --git a/share/smack/include/pthreadtypes.h b/share/smack/include/pthreadtypes.h index f269bccab..151cecc72 100644 --- a/share/smack/include/pthreadtypes.h +++ b/share/smack/include/pthreadtypes.h @@ -25,14 +25,18 @@ typedef int pthread_t; typedef int pthread_attr_t; #endif -typedef struct { int prioceil, proto, pshared, type; } pthread_mutexattr_t; +typedef struct { + int prioceil, proto, pshared, type; +} pthread_mutexattr_t; typedef struct { int lock, init; pthread_mutexattr_t attr; } pthread_mutex_t; -typedef struct { int cond, init; } pthread_cond_t; +typedef struct { + int cond, init; +} pthread_cond_t; typedef int pthread_condattr_t; diff --git a/share/smack/include/smack.h b/share/smack/include/smack.h index 71671b210..e633a01fb 100644 --- a/share/smack/include/smack.h +++ b/share/smack/include/smack.h @@ -30,7 +30,9 @@ void __SMACK_mod(const char *fmt, ...); void __SMACK_decl(const char *fmt, ...); void __SMACK_top_decl(const char *fmt, ...); -typedef struct smack_value { void *dummy; } * smack_value_t; +typedef struct smack_value { + void *dummy; +} * smack_value_t; smack_value_t __SMACK_value(); smack_value_t __SMACK_values(void *ary, unsigned count); smack_value_t __SMACK_return_value(void); diff --git a/test/contracts/failing/array_forall.c b/test/contracts/failing/array_forall.c index 56edd88b7..b57545e5a 100644 --- a/test/contracts/failing/array_forall.c +++ b/test/contracts/failing/array_forall.c @@ -10,14 +10,12 @@ int g[SIZE]; void p() { - ensures(forall("i", - qvar("i", int) < 0 || qvar("i", int) >= SIZE || - g[qvar("i", int)] == qvar("i", int))); + ensures(forall("i", qvar("i", int) < 0 || qvar("i", int) >= SIZE || + g[qvar("i", int)] == qvar("i", int))); for (int i = 0; i < SIZE; i++) { - invariant(forall("x", - qvar("x", int) < 0 || qvar("x", int) >= i || - g[qvar("x", int)] == qvar("x", int))); + invariant(forall("x", qvar("x", int) < 0 || qvar("x", int) >= i || + g[qvar("x", int)] == qvar("x", int))); g[i] = i; } } diff --git a/test/contracts/failing/array_forall_fail.c b/test/contracts/failing/array_forall_fail.c index 1b0f91bb1..45a0f5e18 100644 --- a/test/contracts/failing/array_forall_fail.c +++ b/test/contracts/failing/array_forall_fail.c @@ -10,14 +10,12 @@ int g[SIZE]; void p() { - ensures(forall("i", - qvar("i", int) < 0 || qvar("i", int) >= SIZE || - g[qvar("i", int)] == qvar("i", int))); + ensures(forall("i", qvar("i", int) < 0 || qvar("i", int) >= SIZE || + g[qvar("i", int)] == qvar("i", int))); for (int i = 0; i < SIZE; i++) { - invariant(forall("x", - qvar("x", int) < 0 || qvar("x", int) > i || - g[qvar("x", int)] == qvar("x", int))); + invariant(forall("x", qvar("x", int) < 0 || qvar("x", int) > i || + g[qvar("x", int)] == qvar("x", int))); g[i] = i; } } diff --git a/test/contracts/failing/forall.c b/test/contracts/failing/forall.c index ac0c853eb..5134e4803 100644 --- a/test/contracts/failing/forall.c +++ b/test/contracts/failing/forall.c @@ -8,7 +8,7 @@ int g[10]; int main(void) { - ensures(forall( - "x", g[qvar("x", int)] == 0 || qvar("x", int) < 0 || qvar("x", int) > 9)); + ensures(forall("x", g[qvar("x", int)] == 0 || qvar("x", int) < 0 || + qvar("x", int) > 9)); return 0; } diff --git a/test/contracts/failing/forall_fail.c b/test/contracts/failing/forall_fail.c index 4c3c4b096..bf176b86f 100644 --- a/test/contracts/failing/forall_fail.c +++ b/test/contracts/failing/forall_fail.c @@ -8,8 +8,7 @@ int g[10]; int main(void) { - ensures(forall("x", - g[qvar("x", int)] == 0 || qvar("x", int) < 0 || - qvar("x", int) > 10)); + ensures(forall("x", g[qvar("x", int)] == 0 || qvar("x", int) < 0 || + qvar("x", int) > 10)); return 0; } diff --git a/test/data/struct_cast.c b/test/data/struct_cast.c index 70b2416a2..dd1493b89 100644 --- a/test/data/struct_cast.c +++ b/test/data/struct_cast.c @@ -9,7 +9,9 @@ typedef struct { int b; } S1; -typedef struct { int x; } S2; +typedef struct { + int x; +} S2; int main(void) { S1 s1; diff --git a/test/data/struct_cast1.c b/test/data/struct_cast1.c index 3334729a1..d1e85cd21 100644 --- a/test/data/struct_cast1.c +++ b/test/data/struct_cast1.c @@ -4,7 +4,9 @@ // @expect verified -typedef struct { int x; } S1; +typedef struct { + int x; +} S1; typedef struct { int a; diff --git a/test/data/struct_cast1_fail.c b/test/data/struct_cast1_fail.c index 6e4b9c9ce..91f0bb018 100644 --- a/test/data/struct_cast1_fail.c +++ b/test/data/struct_cast1_fail.c @@ -4,7 +4,9 @@ // @expect error -typedef struct { int x; } S1; +typedef struct { + int x; +} S1; typedef struct { int a; diff --git a/test/data/struct_cast_fail.c b/test/data/struct_cast_fail.c index 1db838233..68f0cfb5a 100644 --- a/test/data/struct_cast_fail.c +++ b/test/data/struct_cast_fail.c @@ -9,7 +9,9 @@ typedef struct { int b; } S1; -typedef struct { int x; } S2; +typedef struct { + int x; +} S2; int main(void) { S1 s1; diff --git a/test/ntdrivers/cdaudio_true.i.cil.c b/test/ntdrivers/cdaudio_true.i.cil.c index 1607b4787..25e9bb22b 100644 --- a/test/ntdrivers/cdaudio_true.i.cil.c +++ b/test/ntdrivers/cdaudio_true.i.cil.c @@ -3135,7 +3135,7 @@ NTSTATUS CdAudioAddDevice(PDRIVER_OBJECT DriverObject, } { /* KeInitializeEvent(& extension->PagingPathCountEvent, 1, 1); */ /* INLINED - */ + */ extension->Active = (unsigned char)regActive; extension->DeviceObject = deviceObject; extension->TargetPdo = PhysicalDeviceObject; diff --git a/test/ntdrivers/floppy2_true.i.cil.c b/test/ntdrivers/floppy2_true.i.cil.c index 678c45494..a9268e30a 100644 --- a/test/ntdrivers/floppy2_true.i.cil.c +++ b/test/ntdrivers/floppy2_true.i.cil.c @@ -4011,7 +4011,7 @@ NTSTATUS DriverEntry(PDRIVER_OBJECT DriverObject, } { #line 276 - __cil_tmp52 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp52 = (KUSER_SHARED_DATA *const)4292804608U; #line 276 __cil_tmp53 = (unsigned int)__cil_tmp52; #line 276 @@ -4043,7 +4043,7 @@ NTSTATUS DriverEntry(PDRIVER_OBJECT DriverObject, } { #line 279 - __cil_tmp62 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp62 = (KUSER_SHARED_DATA *const)4292804608U; #line 279 __cil_tmp63 = (unsigned int)__cil_tmp62; #line 279 @@ -5030,7 +5030,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject, } { #line 505 - __cil_tmp204 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp204 = (KUSER_SHARED_DATA *const)4292804608U; #line 505 __cil_tmp205 = (unsigned int)__cil_tmp204; #line 505 @@ -5423,7 +5423,7 @@ NTSTATUS FlConfigCallBack(PVOID Context, PUNICODE_STRING PathName, { #line 651 __cil_tmp54 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 651 __cil_tmp55 = (unsigned int)__cil_tmp54; #line 651 @@ -8698,7 +8698,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { { #line 1378 __cil_tmp331 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 1378 __cil_tmp332 = (unsigned int)__cil_tmp331; #line 1378 @@ -9248,7 +9248,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { { #line 1478 __cil_tmp456 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 1478 __cil_tmp457 = (unsigned int)__cil_tmp456; #line 1478 @@ -12021,7 +12021,7 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) { if (ntStatus >= 0L) { { #line 1993 - __cil_tmp139 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp139 = (KUSER_SHARED_DATA *const)4292804608U; #line 1993 __cil_tmp140 = (unsigned int)__cil_tmp139; #line 1993 @@ -14569,7 +14569,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, if (__cil_tmp109 != 0) { { #line 2743 - __cil_tmp110 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp110 = (KUSER_SHARED_DATA *const)4292804608U; #line 2743 __cil_tmp111 = (unsigned int)__cil_tmp110; #line 2743 @@ -15105,7 +15105,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } { #line 2903 - __cil_tmp256 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp256 = (KUSER_SHARED_DATA *const)4292804608U; #line 2903 __cil_tmp257 = (unsigned int)__cil_tmp256; #line 2903 @@ -15408,7 +15408,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } else { _L___2 : { #line 3004 - __cil_tmp334 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp334 = (KUSER_SHARED_DATA *const)4292804608U; #line 3004 __cil_tmp335 = (unsigned int)__cil_tmp334; #line 3004 @@ -15611,7 +15611,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } { #line 3085 - __cil_tmp379 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp379 = (KUSER_SHARED_DATA *const)4292804608U; #line 3085 __cil_tmp380 = (unsigned int)__cil_tmp379; #line 3085 @@ -16401,7 +16401,7 @@ NTSTATUS FlRecalibrateDrive(PDISKETTE_EXTENSION DisketteExtension) { if (ntStatus >= 0L) { { #line 3307 - __cil_tmp28 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp28 = (KUSER_SHARED_DATA *const)4292804608U; #line 3307 __cil_tmp29 = (unsigned int)__cil_tmp28; #line 3307 @@ -17157,7 +17157,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { while_101_continue: /* CIL Label */; { #line 3452 - __cil_tmp29 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp29 = (KUSER_SHARED_DATA *const)4292804608U; #line 3452 __cil_tmp30 = (unsigned int)__cil_tmp29; #line 3452 @@ -17409,7 +17409,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { { #line 3502 __cil_tmp111 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 3502 __cil_tmp112 = (unsigned int)__cil_tmp111; #line 3502 @@ -17587,7 +17587,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { _L___0 : { #line 3553 __cil_tmp154 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 3553 __cil_tmp155 = (unsigned int)__cil_tmp154; #line 3553 @@ -17730,8 +17730,8 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { *mem_357 = *__cil_tmp194; { #line 3588 - __cil_tmp195 = (KUSER_SHARED_DATA * - const)4292804608U; + __cil_tmp195 = (KUSER_SHARED_DATA + *const)4292804608U; #line 3588 __cil_tmp196 = (unsigned int)__cil_tmp195; @@ -17799,8 +17799,8 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { *mem_361 = (unsigned long)__cil_tmp207; { #line 3594 - __cil_tmp208 = (KUSER_SHARED_DATA * - const)4292804608U; + __cil_tmp208 = (KUSER_SHARED_DATA + *const)4292804608U; #line 3594 __cil_tmp209 = (unsigned int)__cil_tmp208; @@ -19461,7 +19461,7 @@ void FloppyThread(PVOID Context) { if (waitStatus == 258L) { { #line 3938 - __cil_tmp20 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp20 = (KUSER_SHARED_DATA *const)4292804608U; #line 3938 __cil_tmp21 = (unsigned int)__cil_tmp20; #line 3938 @@ -19648,7 +19648,7 @@ void FloppyThread(PVOID Context) { } { #line 3977 - __cil_tmp75 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp75 = (KUSER_SHARED_DATA *const)4292804608U; #line 3977 __cil_tmp76 = (unsigned int)__cil_tmp75; #line 3977 @@ -20098,7 +20098,7 @@ void FloppyThread(PVOID Context) { _L : { #line 4057 __cil_tmp189 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 4057 __cil_tmp190 = (unsigned int)__cil_tmp189; #line 4057 @@ -20380,7 +20380,7 @@ void FloppyThread(PVOID Context) { { #line 4117 __cil_tmp257 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 4117 __cil_tmp258 = (unsigned int)__cil_tmp257; #line 4117 @@ -20524,7 +20524,7 @@ void FloppyThread(PVOID Context) { { #line 4170 __cil_tmp289 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 4170 __cil_tmp290 = (unsigned int)__cil_tmp289; #line 4170 @@ -21199,8 +21199,8 @@ void FloppyThread(PVOID Context) { { #line 4448 __cil_tmp408 = - (KUSER_SHARED_DATA * - const)4292804608U; + (KUSER_SHARED_DATA + *const)4292804608U; #line 4448 __cil_tmp409 = (unsigned int)__cil_tmp408; @@ -21538,7 +21538,7 @@ void FloppyThread(PVOID Context) { } { #line 4546 - __cil_tmp477 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp477 = (KUSER_SHARED_DATA *const)4292804608U; #line 4546 __cil_tmp478 = (unsigned int)__cil_tmp477; #line 4546 @@ -22099,7 +22099,7 @@ void FlConsolidateMediaTypeWithBootSector(PDISKETTE_EXTENSION DisketteExtension, while_136_continue: /* CIL Label */; { #line 4629 - __cil_tmp95 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp95 = (KUSER_SHARED_DATA *const)4292804608U; #line 4629 __cil_tmp96 = (unsigned int)__cil_tmp95; #line 4629 @@ -22692,7 +22692,7 @@ void FlCheckBootSector(PDISKETTE_EXTENSION DisketteExtension) { { { #line 4776 - __cil_tmp9 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp9 = (KUSER_SHARED_DATA *const)4292804608U; #line 4776 __cil_tmp10 = (unsigned int)__cil_tmp9; #line 4776 @@ -22751,7 +22751,7 @@ void FlCheckBootSector(PDISKETTE_EXTENSION DisketteExtension) { *mem_63 = (unsigned long)__cil_tmp21; { #line 4782 - __cil_tmp22 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp22 = (KUSER_SHARED_DATA *const)4292804608U; #line 4782 __cil_tmp23 = (unsigned int)__cil_tmp22; #line 4782 @@ -23715,7 +23715,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl, { #line 4946 __cil_tmp130 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 4946 __cil_tmp131 = (unsigned int)__cil_tmp130; #line 4946 @@ -24271,7 +24271,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl, if (status >= 0L) { { #line 5030 - __cil_tmp290 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp290 = (KUSER_SHARED_DATA *const)4292804608U; #line 5030 __cil_tmp291 = (unsigned int)__cil_tmp290; #line 5030 @@ -25017,7 +25017,7 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } { #line 5214 - __cil_tmp44 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp44 = (KUSER_SHARED_DATA *const)4292804608U; #line 5214 __cil_tmp45 = (unsigned int)__cil_tmp44; #line 5214 @@ -26589,7 +26589,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { } { #line 5535 - __cil_tmp145 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp145 = (KUSER_SHARED_DATA *const)4292804608U; #line 5535 __cil_tmp146 = (unsigned int)__cil_tmp145; #line 5535 @@ -26860,7 +26860,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { } { #line 5607 - __cil_tmp229 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp229 = (KUSER_SHARED_DATA *const)4292804608U; #line 5607 __cil_tmp230 = (unsigned int)__cil_tmp229; #line 5607 @@ -27515,7 +27515,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { if (!__cil_tmp418) { { #line 5790 - __cil_tmp419 = (KUSER_SHARED_DATA * const)4292804608U; + __cil_tmp419 = (KUSER_SHARED_DATA *const)4292804608U; #line 5790 __cil_tmp420 = (unsigned int)__cil_tmp419; #line 5790 @@ -28132,7 +28132,7 @@ BOOLEAN FlCheckFormatParameters(PDISKETTE_EXTENSION DisketteExtension, { #line 5948 __cil_tmp74 = - (KUSER_SHARED_DATA * const)4292804608U; + (KUSER_SHARED_DATA *const)4292804608U; #line 5948 __cil_tmp75 = (unsigned int)__cil_tmp74; #line 5948 diff --git a/test/ntdrivers/floppy_false.i.cil.c b/test/ntdrivers/floppy_false.i.cil.c index f3b75b3c3..df610e792 100644 --- a/test/ntdrivers/floppy_false.i.cil.c +++ b/test/ntdrivers/floppy_false.i.cil.c @@ -2173,15 +2173,15 @@ NTSTATUS DriverEntry(PDRIVER_OBJECT DriverObject, /* KeInitializeEvent(& PagingMutex->Event, 1, 0); */ /* INLINED */ /* MmPageEntireDriver(& DriverEntry); */ /* INLINED */ } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { DriveMediaLimits = (struct _DRIVE_MEDIA_LIMITS *)(_DriveMediaLimits_NEC98); } else { DriveMediaLimits = _DriveMediaLimits; } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { DriveMediaConstants = _DriveMediaConstants_NEC98; } else { DriveMediaConstants = _DriveMediaConstants; @@ -2228,9 +2228,10 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject, { tmp = i; i = (USHORT)((int)i + 1); - swprintf(deviceNameBuffer, "\\\000D\000e\000v\000i\000c\000e\000\\" - "\000F\000l\000o\000p\000p\000y\000%" - "\000d\000", + swprintf(deviceNameBuffer, + "\\\000D\000e\000v\000i\000c\000e\000\\" + "\000F\000l\000o\000p\000p\000y\000%" + "\000d\000", tmp); /* RtlInitUnicodeString(& deviceName, deviceNameBuffer); */ /* INLINED */ ntStatus = IoCreateDevice(DriverObject, sizeof(DISKETTE_EXTENSION), @@ -2267,7 +2268,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject, fdcInfo.BusNumber, fdcInfo.ControllerNumber, fdcInfo.PeripheralNumber); /* RtlInitString(& arcNameString, arcNameBuffer); */ /* INLINED - */ + */ ntStatus = RtlAnsiStringToUnicodeString(&disketteExtension->ArcName, &arcNameString, 1); } @@ -2318,7 +2319,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject, disketteExtension->IsReadOnly = 0; disketteExtension->MediaType = -1; } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->ControllerConfigurable = 0; } else { @@ -2414,7 +2415,7 @@ NTSTATUS FlConfigCallBack(PVOID Context, PUNICODE_STRING PathName, driveType = 4; goto switch_8_break; switch_8_1201: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { driveType = 5; goto switch_8_break; @@ -2591,7 +2592,7 @@ NTSTATUS FlQueueIrpToThread(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) { irpSp = Irp->Tail.Overlay.__annonCompField17.__annonCompField16 .CurrentStackLocation; /* ExAcquireFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED - */ + */ } if ((int)DisketteExtension->PoweringDown == 1) { { @@ -2605,7 +2606,7 @@ NTSTATUS FlQueueIrpToThread(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) { } { /* ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED - */ + */ } {} { /* ExAcquireFastMutex(& DisketteExtension->ThreadReferenceMutex); */ /* INLINED */ DisketteExtension->ThreadReferenceCount += 1L; @@ -2729,7 +2730,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { irpSp = Irp->Tail.Overlay.__annonCompField17.__annonCompField16 .CurrentStackLocation; /* ExAcquireFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->HoldNewRequests) { if (irpSp->Parameters.DeviceIoControl.IoControlCode != @@ -2745,7 +2746,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } { /* ExReleaseFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->IsRemoved) { { @@ -3034,14 +3035,14 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { outputBuffer->Cylinders.__annonCompField1 .HighPart = 0; outputBuffer->TracksPerCylinder = - (DriveMediaConstants + - i)->NumberOfHeads; + (DriveMediaConstants + i) + ->NumberOfHeads; outputBuffer->SectorsPerTrack = - (DriveMediaConstants + - i)->SectorsPerTrack; + (DriveMediaConstants + i) + ->SectorsPerTrack; outputBuffer->BytesPerSector = - (DriveMediaConstants + - i)->BytesPerSector; + (DriveMediaConstants + i) + ->BytesPerSector; {} outputBuffer += 1; Irp->IoStatus.Information += @@ -3052,8 +3053,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } goto switch_16_break; switch_16_exp_10: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * - const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { {} if (!(DeviceObject->Characteristics & 1UL)) { @@ -3097,11 +3097,12 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { queryTable[0].EntryContext = &driveLetterName; ntStatus = RtlQueryRegistryValues( - 0, "\\\000R\000e\000g\000i\000s\000t" - "\000r\000y\000\\\000M\000a\000c\000" - "h\000i\000n\000e\000\\\000S\000y" - "\000s\000t\000e\000m\000\\\000D\000" - "I\000S\000K\000", + 0, + "\\\000R\000e\000g\000i\000s\000t" + "\000r\000y\000\\\000M\000a\000c\000" + "h\000i\000n\000e\000\\\000S\000y" + "\000s\000t\000e\000m\000\\\000D\000" + "I\000S\000K\000", queryTable, (void *)0, (void *)0); } if (!(ntStatus >= 0L)) { @@ -3170,11 +3171,12 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } { RtlDeleteRegistryValue( - 0, "\\\000R\000e\000g\000i\000s\000t" - "\000r\000y\000\\\000M\000a\000c\000" - "h\000i\000n\000e\000\\\000S\000y" - "\000s\000t\000e\000m\000\\\000D\000" - "I\000S\000K\000", + 0, + "\\\000R\000e\000g\000i\000s\000t" + "\000r\000y\000\\\000M\000a\000c\000" + "h\000i\000n\000e\000\\\000S\000y" + "\000s\000t\000e\000m\000\\\000D\000" + "I\000S\000K\000", valueName); /* ExFreePool(valueName); */ /* INLINED */ memcpy(suggestedName->Name, @@ -3189,8 +3191,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } else { } switch_16_exp_11: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * - const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { {} if (irpSp->Parameters.DeviceIoControl @@ -3276,7 +3277,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { if ((unsigned char)tmp___2) { { /* IoSetHardErrorOrVerifyDevice(Irp, DeviceObject); */ /* INLINED - */ + */ } } else { } @@ -3733,7 +3734,7 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } } if (ntStatus >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->DeviceUnit = (unsigned char)fdcInfo.UnitNumber; disketteExtension->DriveOnValue = (unsigned char)fdcInfo.UnitNumber; @@ -3909,20 +3910,20 @@ NTSTATUS FloppyReadWrite(PDEVICE_OBJECT DeviceObject, PIRP Irp) { irpSp = Irp->Tail.Overlay.__annonCompField17.__annonCompField16 .CurrentStackLocation; /* ExAcquireFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->HoldNewRequests) { { ntStatus = FloppyQueueRequest(disketteExtension, Irp); /* ExReleaseFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } return (ntStatus); } else { } { /* ExReleaseFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->IsRemoved) { goto _L; @@ -4145,9 +4146,9 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, { ntStatus = 0L; - {} * (DriveMediaConstants + - (DriveMediaLimits + DisketteExtension->DriveType) - ->HighestDriveMediaType) = + {} * + (DriveMediaConstants + (DriveMediaLimits + DisketteExtension->DriveType) + ->HighestDriveMediaType) = DisketteExtension->BiosDriveMediaConstants; if ((int)DisketteExtension->MediaType == -1) { DisketteExtension->DriveMediaConstants = *(DriveMediaConstants + 0); @@ -4208,7 +4209,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } else { } if ((int)DisketteExtension->DriveType != 0) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { DisketteExtension->FifoBuffer[0] = 14; @@ -4293,7 +4294,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } } } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { DisketteExtension->FifoBuffer[0] = 14; @@ -4350,7 +4351,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } } else { _L___2: /* CIL Label */ - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { FlHdbit(DisketteExtension); } } else { @@ -4392,7 +4393,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, return (ntStatus); } else { } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (!((int)DisketteExtension->FifoBuffer[0] & 32)) { {} @@ -4505,7 +4506,7 @@ NTSTATUS FlRecalibrateDrive(PDISKETTE_EXTENSION DisketteExtension) { } else { } if (ntStatus >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { fifoBuffer[0] = DisketteExtension->FifoBuffer[0]; @@ -4594,7 +4595,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { { while (1) { while_101_continue: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { sectorLengthCode = @@ -4639,7 +4640,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { if ((int)DisketteExtension->FifoBuffer[2] != 0) { goto _L; } else { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)DisketteExtension->FifoBuffer[6] != (int)sectorLengthCode) { @@ -4669,7 +4670,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { } } else { _L___0: /* CIL Label */ - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { DisketteExtension->MediaType = driveMediaConstants->MediaType; @@ -4684,7 +4685,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { DisketteExtension->DriveMediaConstants = *(DriveMediaConstants + DisketteExtension->DriveMediaType); - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { tmp = 1024; } else { @@ -4702,7 +4703,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { offset.__annonCompField1.HighPart = 0; offset.__annonCompField1.LowPart = offset.__annonCompField1.HighPart; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { tmp___1 = 1024; } else { @@ -4731,7 +4732,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { /* MmUnlockPages(irp->MdlAddress); */ /* INLINED */ /* IoFreeMdl(irp->MdlAddress); */ /* INLINED */ /* IoFreeIrp(irp); */ /* INLINED - */ + */ /* ExFreePool(bootSector); */ /* INLINED */ } if (!(ntStatus >= 0L)) { @@ -4856,7 +4857,7 @@ void FlAllocateIoBuffer(PDISKETTE_EXTENSION DisketteExtension, if (allocateContiguous) { { /* MmFreeContiguousMemory(DisketteExtension->IoBuffer); */ /* INLINED - */ + */ } } else { { /* ExFreePool(DisketteExtension->IoBuffer); */ /* INLINED */ @@ -4871,7 +4872,7 @@ void FlAllocateIoBuffer(PDISKETTE_EXTENSION DisketteExtension, if (allocateContiguous) { { /* MmFreeContiguousMemory(DisketteExtension->IoBuffer); */ /* INLINED - */ + */ } } else { { /* ExFreePool(DisketteExtension->IoBuffer); */ /* INLINED */ @@ -4904,7 +4905,7 @@ void FlFreeIoBuffer(PDISKETTE_EXTENSION DisketteExtension) { if (contiguousBuffer) { { /* MmFreeContiguousMemory(DisketteExtension->IoBuffer); */ /* INLINED - */ + */ } } else { { /* ExFreePool(DisketteExtension->IoBuffer); */ /* INLINED */ @@ -4945,7 +4946,7 @@ void FloppyThread(PVOID Context) { &queueWait); } if (waitStatus == 258L) { - if (!((int)((KUSER_SHARED_DATA * const)4292804608U) + if (!((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1)) { if (disketteExtension->FloppyControllerAllocated) { {} { @@ -4976,7 +4977,7 @@ void FloppyThread(PVOID Context) { { /* ExReleaseFastMutex(& disketteExtension->ThreadReferenceMutex); */ /* INLINED */ } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (disketteExtension->ReleaseFdcWithMotorRunning) { { @@ -5085,7 +5086,7 @@ void FloppyThread(PVOID Context) { } else { if ((int)irpSp->MinorFunction == 5) { _L: /* CIL Label */ - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (disketteExtension ->ReleaseFdcWithMotorRunning) { @@ -5125,7 +5126,7 @@ void FloppyThread(PVOID Context) { if (PagingReferenceCount == 0UL) { { /* MmPageEntireDriver(& DriverEntry); */ /* INLINED - */ + */ } } else { } @@ -5148,7 +5149,7 @@ void FloppyThread(PVOID Context) { } if (ntStatus >= 0L) { disketteExtension->FloppyControllerAllocated = 1; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->ReleaseFdcWithMotorRunning = 0; } else { @@ -5180,7 +5181,7 @@ void FloppyThread(PVOID Context) { } if (ntStatus >= 0L) { disketteExtension->FloppyControllerAllocated = 1; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->ReleaseFdcWithMotorRunning = 0; } else { @@ -5356,8 +5357,8 @@ void FloppyThread(PVOID Context) { } goto switch_125_break; switch_125_exp_18: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * - const)4292804608U) + if ((int)((KUSER_SHARED_DATA + *const)4292804608U) ->AlternativeArchitecture == 1) { { @@ -5450,7 +5451,7 @@ void FloppyThread(PVOID Context) { } while_117_break: /* CIL Label */; } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (disketteExtension->FloppyControllerAllocated) { { @@ -5520,7 +5521,7 @@ void FlConsolidateMediaTypeWithBootSector(PDISKETTE_EXTENSION DisketteExtension, { while (1) { while_136_continue: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { tmp = 21; } else { @@ -5681,8 +5682,8 @@ void FlCheckBootSector(PDISKETTE_EXTENSION DisketteExtension) { int tmp___1; { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { tmp = 1024; } else { tmp = 512; @@ -5697,8 +5698,8 @@ void FlCheckBootSector(PDISKETTE_EXTENSION DisketteExtension) { } offset.__annonCompField1.HighPart = 0; offset.__annonCompField1.LowPart = offset.__annonCompField1.HighPart; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { tmp___1 = 1024; } else { tmp___1 = 512; @@ -5807,7 +5808,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl, DisketteExtension->FifoBuffer, (void *)0, 0, 0); } if (status >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)DisketteExtension->FifoBuffer[0] & 8) { return (-1073741661L); @@ -5903,7 +5904,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl, IoOffset, transferBytes); } if (status >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)DisketteExtension->FifoBuffer[0] & 8) { return (-1073741661L); @@ -6062,8 +6063,8 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, return (status); } else { } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { { FlHdbit(DisketteExtension); } } else { } @@ -6298,8 +6299,8 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { (ULONG)driveMediaConstants->NumberOfHeads + formatParameters->EndHeadNumber); {} - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { { FlHdbit(DisketteExtension); } } else { } @@ -6340,7 +6341,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { headSettleTime.__annonCompField1.HighPart = -1; KeDelayExecutionThread(0, 0, &headSettleTime); } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { } else { @@ -6462,7 +6463,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { while_175_break: /* CIL Label */; } if (!(ntStatus >= 0L)) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { DisketteExtension->FifoBuffer[0] = 14; @@ -6580,7 +6581,7 @@ BOOLEAN FlCheckFormatParameters(PDISKETTE_EXTENSION DisketteExtension, FormatParameters->StartCylinderNumber) { return (0); } else { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)FormatParameters->MediaType == 6) { return (0); diff --git a/test/ntdrivers/floppy_true.i.cil.c b/test/ntdrivers/floppy_true.i.cil.c index c9b9791fc..deb7c036b 100644 --- a/test/ntdrivers/floppy_true.i.cil.c +++ b/test/ntdrivers/floppy_true.i.cil.c @@ -2173,15 +2173,15 @@ NTSTATUS DriverEntry(PDRIVER_OBJECT DriverObject, /* KeInitializeEvent(& PagingMutex->Event, 1, 0); */ /* INLINED */ /* MmPageEntireDriver(& DriverEntry); */ /* INLINED */ } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { DriveMediaLimits = (struct _DRIVE_MEDIA_LIMITS *)(_DriveMediaLimits_NEC98); } else { DriveMediaLimits = _DriveMediaLimits; } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { DriveMediaConstants = _DriveMediaConstants_NEC98; } else { DriveMediaConstants = _DriveMediaConstants; @@ -2228,9 +2228,10 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject, { tmp = i; i = (USHORT)((int)i + 1); - swprintf(deviceNameBuffer, "\\\000D\000e\000v\000i\000c\000e\000\\" - "\000F\000l\000o\000p\000p\000y\000%" - "\000d\000", + swprintf(deviceNameBuffer, + "\\\000D\000e\000v\000i\000c\000e\000\\" + "\000F\000l\000o\000p\000p\000y\000%" + "\000d\000", tmp); /* RtlInitUnicodeString(& deviceName, deviceNameBuffer); */ /* INLINED */ ntStatus = IoCreateDevice(DriverObject, sizeof(DISKETTE_EXTENSION), @@ -2267,7 +2268,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject, fdcInfo.BusNumber, fdcInfo.ControllerNumber, fdcInfo.PeripheralNumber); /* RtlInitString(& arcNameString, arcNameBuffer); */ /* INLINED - */ + */ ntStatus = RtlAnsiStringToUnicodeString(&disketteExtension->ArcName, &arcNameString, 1); } @@ -2318,7 +2319,7 @@ NTSTATUS FloppyAddDevice(PDRIVER_OBJECT DriverObject, disketteExtension->IsReadOnly = 0; disketteExtension->MediaType = -1; } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->ControllerConfigurable = 0; } else { @@ -2414,7 +2415,7 @@ NTSTATUS FlConfigCallBack(PVOID Context, PUNICODE_STRING PathName, driveType = 4; goto switch_8_break; switch_8_1201: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { driveType = 5; goto switch_8_break; @@ -2591,7 +2592,7 @@ NTSTATUS FlQueueIrpToThread(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) { irpSp = Irp->Tail.Overlay.__annonCompField17.__annonCompField16 .CurrentStackLocation; /* ExAcquireFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED - */ + */ } if ((int)DisketteExtension->PoweringDown == 1) { { @@ -2605,7 +2606,7 @@ NTSTATUS FlQueueIrpToThread(PIRP Irp, PDISKETTE_EXTENSION DisketteExtension) { } { /* ExReleaseFastMutex(& DisketteExtension->PowerDownMutex); */ /* INLINED - */ + */ } {} { /* ExAcquireFastMutex(& DisketteExtension->ThreadReferenceMutex); */ /* INLINED */ DisketteExtension->ThreadReferenceCount += 1L; @@ -2729,7 +2730,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { irpSp = Irp->Tail.Overlay.__annonCompField17.__annonCompField16 .CurrentStackLocation; /* ExAcquireFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->HoldNewRequests) { if (irpSp->Parameters.DeviceIoControl.IoControlCode != @@ -2745,7 +2746,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } { /* ExReleaseFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->IsRemoved) { { @@ -3034,14 +3035,14 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { outputBuffer->Cylinders.__annonCompField1 .HighPart = 0; outputBuffer->TracksPerCylinder = - (DriveMediaConstants + - i)->NumberOfHeads; + (DriveMediaConstants + i) + ->NumberOfHeads; outputBuffer->SectorsPerTrack = - (DriveMediaConstants + - i)->SectorsPerTrack; + (DriveMediaConstants + i) + ->SectorsPerTrack; outputBuffer->BytesPerSector = - (DriveMediaConstants + - i)->BytesPerSector; + (DriveMediaConstants + i) + ->BytesPerSector; {} outputBuffer += 1; Irp->IoStatus.Information += @@ -3052,8 +3053,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } goto switch_16_break; switch_16_exp_10: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * - const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { {} if (!(DeviceObject->Characteristics & 1UL)) { @@ -3097,11 +3097,12 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { queryTable[0].EntryContext = &driveLetterName; ntStatus = RtlQueryRegistryValues( - 0, "\\\000R\000e\000g\000i\000s\000t" - "\000r\000y\000\\\000M\000a\000c\000" - "h\000i\000n\000e\000\\\000S\000y" - "\000s\000t\000e\000m\000\\\000D\000" - "I\000S\000K\000", + 0, + "\\\000R\000e\000g\000i\000s\000t" + "\000r\000y\000\\\000M\000a\000c\000" + "h\000i\000n\000e\000\\\000S\000y" + "\000s\000t\000e\000m\000\\\000D\000" + "I\000S\000K\000", queryTable, (void *)0, (void *)0); } if (!(ntStatus >= 0L)) { @@ -3170,11 +3171,12 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } { RtlDeleteRegistryValue( - 0, "\\\000R\000e\000g\000i\000s\000t" - "\000r\000y\000\\\000M\000a\000c\000" - "h\000i\000n\000e\000\\\000S\000y" - "\000s\000t\000e\000m\000\\\000D\000" - "I\000S\000K\000", + 0, + "\\\000R\000e\000g\000i\000s\000t" + "\000r\000y\000\\\000M\000a\000c\000" + "h\000i\000n\000e\000\\\000S\000y" + "\000s\000t\000e\000m\000\\\000D\000" + "I\000S\000K\000", valueName); /* ExFreePool(valueName); */ /* INLINED */ memcpy(suggestedName->Name, @@ -3189,8 +3191,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } else { } switch_16_exp_11: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * - const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { {} if (irpSp->Parameters.DeviceIoControl @@ -3276,7 +3277,7 @@ NTSTATUS FloppyDeviceControl(PDEVICE_OBJECT DeviceObject, PIRP Irp) { if ((unsigned char)tmp___2) { { /* IoSetHardErrorOrVerifyDevice(Irp, DeviceObject); */ /* INLINED - */ + */ } } else { } @@ -3733,7 +3734,7 @@ NTSTATUS FloppyStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } } if (ntStatus >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->DeviceUnit = (unsigned char)fdcInfo.UnitNumber; disketteExtension->DriveOnValue = (unsigned char)fdcInfo.UnitNumber; @@ -3909,20 +3910,20 @@ NTSTATUS FloppyReadWrite(PDEVICE_OBJECT DeviceObject, PIRP Irp) { irpSp = Irp->Tail.Overlay.__annonCompField17.__annonCompField16 .CurrentStackLocation; /* ExAcquireFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->HoldNewRequests) { { ntStatus = FloppyQueueRequest(disketteExtension, Irp); /* ExReleaseFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } return (ntStatus); } else { } { /* ExReleaseFastMutex(& disketteExtension->HoldNewReqMutex); */ /* INLINED - */ + */ } if (disketteExtension->IsRemoved) { goto _L; @@ -4145,9 +4146,9 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, { ntStatus = 0L; - {} * (DriveMediaConstants + - (DriveMediaLimits + DisketteExtension->DriveType) - ->HighestDriveMediaType) = + {} * + (DriveMediaConstants + (DriveMediaLimits + DisketteExtension->DriveType) + ->HighestDriveMediaType) = DisketteExtension->BiosDriveMediaConstants; if ((int)DisketteExtension->MediaType == -1) { DisketteExtension->DriveMediaConstants = *(DriveMediaConstants + 0); @@ -4208,7 +4209,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } else { } if ((int)DisketteExtension->DriveType != 0) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { DisketteExtension->FifoBuffer[0] = 14; @@ -4293,7 +4294,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } } } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { DisketteExtension->FifoBuffer[0] = 14; @@ -4350,7 +4351,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, } } else { _L___2: /* CIL Label */ - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { FlHdbit(DisketteExtension); } } else { @@ -4392,7 +4393,7 @@ NTSTATUS FlStartDrive(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, return (ntStatus); } else { } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (!((int)DisketteExtension->FifoBuffer[0] & 32)) { {} @@ -4505,7 +4506,7 @@ NTSTATUS FlRecalibrateDrive(PDISKETTE_EXTENSION DisketteExtension) { } else { } if (ntStatus >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { fifoBuffer[0] = DisketteExtension->FifoBuffer[0]; @@ -4594,7 +4595,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { { while (1) { while_101_continue: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { sectorLengthCode = @@ -4639,7 +4640,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { if ((int)DisketteExtension->FifoBuffer[2] != 0) { goto _L; } else { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)DisketteExtension->FifoBuffer[6] != (int)sectorLengthCode) { @@ -4669,7 +4670,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { } } else { _L___0: /* CIL Label */ - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { DisketteExtension->MediaType = driveMediaConstants->MediaType; @@ -4684,7 +4685,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { DisketteExtension->DriveMediaConstants = *(DriveMediaConstants + DisketteExtension->DriveMediaType); - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { tmp = 1024; } else { @@ -4702,7 +4703,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { offset.__annonCompField1.HighPart = 0; offset.__annonCompField1.LowPart = offset.__annonCompField1.HighPart; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { tmp___1 = 1024; } else { @@ -4731,7 +4732,7 @@ NTSTATUS FlDetermineMediaType(PDISKETTE_EXTENSION DisketteExtension) { /* MmUnlockPages(irp->MdlAddress); */ /* INLINED */ /* IoFreeMdl(irp->MdlAddress); */ /* INLINED */ /* IoFreeIrp(irp); */ /* INLINED - */ + */ /* ExFreePool(bootSector); */ /* INLINED */ } if (!(ntStatus >= 0L)) { @@ -4856,7 +4857,7 @@ void FlAllocateIoBuffer(PDISKETTE_EXTENSION DisketteExtension, if (allocateContiguous) { { /* MmFreeContiguousMemory(DisketteExtension->IoBuffer); */ /* INLINED - */ + */ } } else { { /* ExFreePool(DisketteExtension->IoBuffer); */ /* INLINED */ @@ -4871,7 +4872,7 @@ void FlAllocateIoBuffer(PDISKETTE_EXTENSION DisketteExtension, if (allocateContiguous) { { /* MmFreeContiguousMemory(DisketteExtension->IoBuffer); */ /* INLINED - */ + */ } } else { { /* ExFreePool(DisketteExtension->IoBuffer); */ /* INLINED */ @@ -4904,7 +4905,7 @@ void FlFreeIoBuffer(PDISKETTE_EXTENSION DisketteExtension) { if (contiguousBuffer) { { /* MmFreeContiguousMemory(DisketteExtension->IoBuffer); */ /* INLINED - */ + */ } } else { { /* ExFreePool(DisketteExtension->IoBuffer); */ /* INLINED */ @@ -4945,7 +4946,7 @@ void FloppyThread(PVOID Context) { &queueWait); } if (waitStatus == 258L) { - if (!((int)((KUSER_SHARED_DATA * const)4292804608U) + if (!((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1)) { if (disketteExtension->FloppyControllerAllocated) { {} { @@ -4976,7 +4977,7 @@ void FloppyThread(PVOID Context) { { /* ExReleaseFastMutex(& disketteExtension->ThreadReferenceMutex); */ /* INLINED */ } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (disketteExtension->ReleaseFdcWithMotorRunning) { { @@ -5085,7 +5086,7 @@ void FloppyThread(PVOID Context) { } else { if ((int)irpSp->MinorFunction == 5) { _L: /* CIL Label */ - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (disketteExtension ->ReleaseFdcWithMotorRunning) { @@ -5125,7 +5126,7 @@ void FloppyThread(PVOID Context) { if (PagingReferenceCount == 0UL) { { /* MmPageEntireDriver(& DriverEntry); */ /* INLINED - */ + */ } } else { } @@ -5148,7 +5149,7 @@ void FloppyThread(PVOID Context) { } if (ntStatus >= 0L) { disketteExtension->FloppyControllerAllocated = 1; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->ReleaseFdcWithMotorRunning = 0; } else { @@ -5180,7 +5181,7 @@ void FloppyThread(PVOID Context) { } if (ntStatus >= 0L) { disketteExtension->FloppyControllerAllocated = 1; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { disketteExtension->ReleaseFdcWithMotorRunning = 0; } else { @@ -5356,8 +5357,8 @@ void FloppyThread(PVOID Context) { } goto switch_125_break; switch_125_exp_18: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * - const)4292804608U) + if ((int)((KUSER_SHARED_DATA + *const)4292804608U) ->AlternativeArchitecture == 1) { { @@ -5450,7 +5451,7 @@ void FloppyThread(PVOID Context) { } while_117_break: /* CIL Label */; } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if (disketteExtension->FloppyControllerAllocated) { { @@ -5520,7 +5521,7 @@ void FlConsolidateMediaTypeWithBootSector(PDISKETTE_EXTENSION DisketteExtension, { while (1) { while_136_continue: /* CIL Label */; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { tmp = 21; } else { @@ -5681,8 +5682,8 @@ void FlCheckBootSector(PDISKETTE_EXTENSION DisketteExtension) { int tmp___1; { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { tmp = 1024; } else { tmp = 512; @@ -5697,8 +5698,8 @@ void FlCheckBootSector(PDISKETTE_EXTENSION DisketteExtension) { } offset.__annonCompField1.HighPart = 0; offset.__annonCompField1.LowPart = offset.__annonCompField1.HighPart; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { tmp___1 = 1024; } else { tmp___1 = 512; @@ -5807,7 +5808,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl, DisketteExtension->FifoBuffer, (void *)0, 0, 0); } if (status >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)DisketteExtension->FifoBuffer[0] & 8) { return (-1073741661L); @@ -5903,7 +5904,7 @@ NTSTATUS FlReadWriteTrack(PDISKETTE_EXTENSION DisketteExtension, PMDL IoMdl, IoOffset, transferBytes); } if (status >= 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)DisketteExtension->FifoBuffer[0] & 8) { return (-1073741661L); @@ -6062,8 +6063,8 @@ NTSTATUS FlReadWrite(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp, return (status); } else { } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { { FlHdbit(DisketteExtension); } } else { } @@ -6298,8 +6299,8 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { (ULONG)driveMediaConstants->NumberOfHeads + formatParameters->EndHeadNumber); {} - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture == 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture == + 1) { { FlHdbit(DisketteExtension); } } else { } @@ -6340,7 +6341,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { headSettleTime.__annonCompField1.HighPart = -1; KeDelayExecutionThread(0, 0, &headSettleTime); } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { } else { @@ -6462,7 +6463,7 @@ NTSTATUS FlFormat(PDISKETTE_EXTENSION DisketteExtension, PIRP Irp) { while_175_break: /* CIL Label */; } if (!(ntStatus >= 0L)) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { DisketteExtension->FifoBuffer[0] = 14; @@ -6580,7 +6581,7 @@ BOOLEAN FlCheckFormatParameters(PDISKETTE_EXTENSION DisketteExtension, FormatParameters->StartCylinderNumber) { return (0); } else { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { if ((int)FormatParameters->MediaType == 6) { return (0); diff --git a/test/ntdrivers/parport_false.i.cil.c b/test/ntdrivers/parport_false.i.cil.c index c9bd3086f..25a8f2d41 100644 --- a/test/ntdrivers/parport_false.i.cil.c +++ b/test/ntdrivers/parport_false.i.cil.c @@ -2920,18 +2920,18 @@ PptRemovePptRemovalRelation(PDEVICE_EXTENSION Extension, if ((unsigned int)listHead->Flink == (unsigned int)listHead) { {} { /* ExReleaseFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } return (0L); } else { {} { /* ExReleaseFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } } { /* ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } { while (1) { while_27_continue: /* CIL Label */; @@ -3016,7 +3016,7 @@ void PptDumpRemovalRelationsList(PDEVICE_EXTENSION Extension) { if ((unsigned int)listHead->Flink == (unsigned int)listHead) { {} { /* ExReleaseFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } return; } else { @@ -3614,9 +3614,8 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject, } else { { Status = PptTrySelectDevice( - Extension, - Irp->AssociatedIrp - .SystemBuffer); + Extension, Irp->AssociatedIrp + .SystemBuffer); IoAcquireCancelSpinLock( &CancelIrql); } @@ -3912,12 +3911,12 @@ NTSTATUS PptDispatchClose(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } { /* ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED - */ + */ } {} } else { { /* ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED - */ + */ } {} } { @@ -6529,10 +6528,10 @@ NTSTATUS PptPnpStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) { if (status >= 0L) { { /* ExAcquireFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ extension->DeviceStateFlags |= 1UL; /* ExReleaseFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ } } else { } @@ -6579,8 +6578,8 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp, goto targetExit; } else { } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture != 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture != + 1) { { tmp = PptIsPci(Extension, Irp); } if (1 == (int)tmp) { {} { @@ -6658,7 +6657,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp, .__annonCompField1.LowPart == 0UL) { if (Extension->PnpInfo.OriginalEcpController .__annonCompField1.HighPart == 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture != 1) { if (PartialResourceDescriptor->u.Port.Start .__annonCompField1.LowPart < @@ -7215,10 +7214,10 @@ NTSTATUS PptPnpQueryStopDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) { myStatus = 0L; status = PptPnpPassThroughPnpIrpAndReleaseRemoveLock(extension, Irp); /* ExAcquireFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ extension->DeviceStateFlags |= 65552UL; /* ExReleaseFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ } } return (status); @@ -7681,7 +7680,7 @@ NTSTATUS PptDispatchPower(PDEVICE_OBJECT pDeviceObject, PIRP pIrp) { if ((int)powerState.DeviceState < (int)Extension->DeviceState) { hookit = 1; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { InitNEC_98(Extension); } } else { @@ -8802,7 +8801,7 @@ NTSTATUS PptInitializeDeviceExtension(PDRIVER_OBJECT DriverObject, Extension->OpenCloseMutex.Count = 1; Extension->OpenCloseMutex.Contention = 0; /* KeInitializeEvent(& Extension->OpenCloseMutex.Event, 1, 0); */ /* INLINED - */ + */ Extension->ExtensionFastMutex.Count = 1; Extension->ExtensionFastMutex.Contention = 0; /* KeInitializeEvent(& Extension->ExtensionFastMutex.Event, 1, 0); */ /* INLINED */ @@ -8844,7 +8843,7 @@ NTSTATUS PptInitializeDeviceExtension(PDRIVER_OBJECT DriverObject, Extension->DeviceName.Length = 0; Extension->DeviceName.MaximumLength = UniNameString->MaximumLength; /* RtlCopyUnicodeString(& Extension->DeviceName, UniNameString); */ /* INLINED - */ + */ Extension->PnpInfo.CurrentMode = 0; Extension_FilterMode = 0; } diff --git a/test/ntdrivers/parport_true.i.cil.c b/test/ntdrivers/parport_true.i.cil.c index 44af56f2d..4d417f898 100644 --- a/test/ntdrivers/parport_true.i.cil.c +++ b/test/ntdrivers/parport_true.i.cil.c @@ -2920,18 +2920,18 @@ PptRemovePptRemovalRelation(PDEVICE_EXTENSION Extension, if ((unsigned int)listHead->Flink == (unsigned int)listHead) { {} { /* ExReleaseFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } return (0L); } else { {} { /* ExReleaseFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } } { /* ExAcquireFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } { while (1) { while_27_continue: /* CIL Label */; @@ -3016,7 +3016,7 @@ void PptDumpRemovalRelationsList(PDEVICE_EXTENSION Extension) { if ((unsigned int)listHead->Flink == (unsigned int)listHead) { {} { /* ExReleaseFastMutex(& Extension->ExtensionFastMutex); */ /* INLINED - */ + */ } return; } else { @@ -3614,9 +3614,8 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject, } else { { Status = PptTrySelectDevice( - Extension, - Irp->AssociatedIrp - .SystemBuffer); + Extension, Irp->AssociatedIrp + .SystemBuffer); IoAcquireCancelSpinLock( &CancelIrql); } @@ -3912,12 +3911,12 @@ NTSTATUS PptDispatchClose(PDEVICE_OBJECT DeviceObject, PIRP Irp) { } { /* ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED - */ + */ } {} } else { { /* ExReleaseFastMutex(& extension->OpenCloseMutex); */ /* INLINED - */ + */ } {} } { @@ -6529,10 +6528,10 @@ NTSTATUS PptPnpStartDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) { if (status >= 0L) { { /* ExAcquireFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ extension->DeviceStateFlags |= 1UL; /* ExReleaseFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ } } else { } @@ -6579,8 +6578,8 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp, goto targetExit; } else { } - if ((int)((KUSER_SHARED_DATA * const)4292804608U) - ->AlternativeArchitecture != 1) { + if ((int)((KUSER_SHARED_DATA *const)4292804608U)->AlternativeArchitecture != + 1) { { tmp = PptIsPci(Extension, Irp); } if (1 == (int)tmp) { {} { @@ -6658,7 +6657,7 @@ NTSTATUS PptPnpStartScanCmResourceList(PDEVICE_EXTENSION Extension, PIRP Irp, .__annonCompField1.LowPart == 0UL) { if (Extension->PnpInfo.OriginalEcpController .__annonCompField1.HighPart == 0L) { - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture != 1) { if (PartialResourceDescriptor->u.Port.Start .__annonCompField1.LowPart < @@ -7215,10 +7214,10 @@ NTSTATUS PptPnpQueryStopDevice(PDEVICE_OBJECT DeviceObject, PIRP Irp) { myStatus = 0L; status = PptPnpPassThroughPnpIrpAndReleaseRemoveLock(extension, Irp); /* ExAcquireFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ extension->DeviceStateFlags |= 65552UL; /* ExReleaseFastMutex(& extension->ExtensionFastMutex); */ /* INLINED - */ + */ } } return (status); @@ -7681,7 +7680,7 @@ NTSTATUS PptDispatchPower(PDEVICE_OBJECT pDeviceObject, PIRP pIrp) { if ((int)powerState.DeviceState < (int)Extension->DeviceState) { hookit = 1; - if ((int)((KUSER_SHARED_DATA * const)4292804608U) + if ((int)((KUSER_SHARED_DATA *const)4292804608U) ->AlternativeArchitecture == 1) { { InitNEC_98(Extension); } } else { @@ -8802,7 +8801,7 @@ NTSTATUS PptInitializeDeviceExtension(PDRIVER_OBJECT DriverObject, Extension->OpenCloseMutex.Count = 1; Extension->OpenCloseMutex.Contention = 0; /* KeInitializeEvent(& Extension->OpenCloseMutex.Event, 1, 0); */ /* INLINED - */ + */ Extension->ExtensionFastMutex.Count = 1; Extension->ExtensionFastMutex.Contention = 0; /* KeInitializeEvent(& Extension->ExtensionFastMutex.Event, 1, 0); */ /* INLINED */ @@ -8844,7 +8843,7 @@ NTSTATUS PptInitializeDeviceExtension(PDRIVER_OBJECT DriverObject, Extension->DeviceName.Length = 0; Extension->DeviceName.MaximumLength = UniNameString->MaximumLength; /* RtlCopyUnicodeString(& Extension->DeviceName, UniNameString); */ /* INLINED - */ + */ Extension->PnpInfo.CurrentMode = 0; Extension_FilterMode = 0; } From 702bd31b7d31f64fa99e42c1a2374960bcd1c791 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Thu, 18 Jul 2019 02:32:07 -0600 Subject: [PATCH 17/20] Added needed additional clang options into documentation as well --- docs/running.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/running.md b/docs/running.md index 48d845603..984d7b47e 100644 --- a/docs/running.md +++ b/docs/running.md @@ -107,7 +107,7 @@ SMACK should report no errors for this example. Under the hood, SMACK first compiles the example into an LLVM bitcode file using Clang: ```Shell -clang -c -Wall -emit-llvm -O0 -g -I../../share/smack/include simple.c -o simple.bc +clang -c -Wall -emit-llvm -O0 -g -Xclang -disable-O0-optnone -I../../share/smack/include simple.c -o simple.bc ``` We use the `-g` flag to compile with debug information enabled, which the SMACK verifier leverages to generate more informative error traces. Then, the generated bitcode From eb4150c1decfe8b105e44fdf9df7c26031584e28 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Sun, 21 Jul 2019 02:45:21 -0600 Subject: [PATCH 18/20] Updated LLVM version in the cmake file --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9c39d3fce..1d4934873 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -6,7 +6,7 @@ cmake_minimum_required(VERSION 2.8) project(smack) if (NOT WIN32 OR MSYS OR CYGWIN) - find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-4.0 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config") + find_program(LLVM_CONFIG_EXECUTABLE NAMES llvm-config-5.0 llvm-config PATHS ${LLVM_CONFIG} DOC "llvm-config") if (LLVM_CONFIG_EXECUTABLE STREQUAL "LLVM_CONFIG_EXECUTABLE-NOTFOUND") message(FATAL_ERROR "llvm-config could not be found!") From 95c012cf182a3896d7cd4261be8074fa87994314 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 21 Jul 2019 22:14:17 +0000 Subject: [PATCH 19/20] Remove temporary files when sigterm is received Handles #419 --- share/smack/top.py | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/share/smack/top.py b/share/smack/top.py index b51b5fc59..4d550070d 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -9,6 +9,7 @@ import sys import shlex import subprocess +import signal from svcomp.utils import verify_bpl_svcomp from utils import temporary_file, try_command, remove_temp_files from replay import replay_error_trace @@ -642,6 +643,14 @@ def smackdOutput(corralOutput): json_string = json.dumps(json_data) return json_string +def clean_up_upon_sigterm(main): + def handler(signum, frame): + remove_temp_files() + sys.exit(0) + signal.signal(signal.SIGTERM, handler) + return main + +@clean_up_upon_sigterm def main(): try: global args From 9673d8b0fc716f6011f7b7766a5ac232f721eef6 Mon Sep 17 00:00:00 2001 From: Zvonimir Date: Thu, 25 Jul 2019 10:28:14 -0600 Subject: [PATCH 20/20] Bumped version number to 2.1.0 --- Doxyfile | 2 +- share/smack/reach.py | 2 +- share/smack/top.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Doxyfile b/Doxyfile index 22256367a..2b459766a 100644 --- a/Doxyfile +++ b/Doxyfile @@ -5,7 +5,7 @@ #--------------------------------------------------------------------------- DOXYFILE_ENCODING = UTF-8 PROJECT_NAME = smack -PROJECT_NUMBER = 2.0.0 +PROJECT_NUMBER = 2.1.0 PROJECT_BRIEF = "A bounded software verifier." PROJECT_LOGO = OUTPUT_DIRECTORY = docs diff --git a/share/smack/reach.py b/share/smack/reach.py index cfeaf692b..ab212e1f2 100755 --- a/share/smack/reach.py +++ b/share/smack/reach.py @@ -11,7 +11,7 @@ from smackgen import * from smackverify import * -VERSION = '2.0.0' +VERSION = '2.1.0' def reachParser(): parser = argparse.ArgumentParser(add_help=False, parents=[verifyParser()]) diff --git a/share/smack/top.py b/share/smack/top.py index 4d550070d..e3927fd28 100755 --- a/share/smack/top.py +++ b/share/smack/top.py @@ -15,7 +15,7 @@ from replay import replay_error_trace from frontend import link_bc_files, frontends, languages, extra_libs -VERSION = '2.0.0' +VERSION = '2.1.0' def results(args): """A dictionary of the result output messages."""