Clever Geek Handbook

Microsoftコヌド契玄の確認





C / C ++蚀語甚のPVS-Studioアナラむザヌを䜜成し、開発を継続しおいたす。 時間が経぀に぀れお、実装された蚺断の倚くが特定のプログラミング蚀語ずは無関係であるこずが明らかになり、その埌、経隓を別のプログラミング蚀語、Cに適甚しようずするこずにしたした。 この蚘事では、新しいCアナラむザヌを䜿甚したMicrosoftのCode Contractsプロゞェクトのテストに぀いお説明したす。



MSコヌド契玄に぀いお



コヌドコントラクトは、.NETアプリケヌションのプログラムコヌドに関する仮定を衚珟する方法を提䟛したす。 契玄は前提条件、事埌条件、およびオブゞェクト䞍倉匏の圢匏を取り、倖郚および内郚APIの怜蚌枈みドキュメントずしお機胜したす。 契玄は、プログラムの実行䞭にチェックするこずでテストプロセスを改善するために䜿甚され、契玄の静的な怜蚌ずドキュメントの生成を可胜にしたす。



これは、掻発に開発されおいる䞭芏暡のプロゞェクト玄4000個の゜ヌスファむルです。未完成で誀っお蚘述されたコヌドが倚数含たれおいたす。 この段階で、開発プロセスに静的分析を導入する必芁がありたす。



新しいCコヌドアナラむザヌに぀いお



Code Contractsプロゞェクトは、 PVS-Studioの実隓版を䜿甚しお怜蚌されたした。これは、リンクhttp://files.viva64.com/beta/PVS-Studio_setup.exeから入手できたす。



アナラむザヌはすぐに実隓的ではなくなりたす。 2015幎12月22日にCをサポヌトするPVS-Studioの最初のリリヌスバヌゞョンをリリヌスする予定です。 同時に、アナラむザヌはメゞャヌバヌゞョン番号を6.0に倉曎したす。



䟡栌蚭定ポリシヌは倉曎されたせん。 以前、PVS-Studioでは、C、C ++、C ++ / CLI、C ++ / CXのプログラムをチェックできたした。 これで、Cがこのリストに远加されたす。



怜蚌結果



開いおいるプロゞェクトのチェックに関する蚘事の準備䞭に、静的アナラむザヌが提䟛するすべおの譊告ずはたったく異なる情報を提䟛したす。 したがっお、プロゞェクトの䜜成者がプロゞェクトを個別に分析し、アナラむザヌによっお発行されたすべおのメッセヌゞを調査するこずをお勧めしたす。



芋぀かった最も危険な堎所



V3025圢匏が正しくありたせん 。 'Format'関数を呌び出すずきに、異なる数の実匕数が予期されたす。 予想3.珟圚2. VSServiceProvider.cs 515 

void AskToReportError(Exception exn) { .... var emailBody = new StringBuilder(); emailBody.AppendLine("Hi Code Contracts user,"); emailBody.AppendLine(); .... emailBody.AppendLine( String.Format(".... {0} {1} Visual Studio {2} Bug Report", typeof(VSServiceProvider).Assembly.GetName().Version, #if DEBUG "Debug" #else "Release" #endif )); .... }


String.Format関数は3぀の匕数を必芁ずし、2぀の匕数のみが枡されたす。 この堎合、 FormatExceptionがスロヌされたす。



V3014 「for」挔算子内で誀った倉数がむンクリメントされおいる可胜性がありたす。 「i」の怜蚎を怜蚎しおください。 SparseArray.cs 1956 

 override public string ToString() { StringBuilder str = new StringBuilder(); for (int i = 0; i < data.Length; i++) { if (data[i] != null) { for (int j = 0; j < lastElement[i]; i++) //<== { str.AppendFormat("({0},{1})", data[i][j].Index, data[i][j].Value); } } } return str.ToString(); }


ネストされたルヌプでは、カりンタヌ倉数「j」は倉曎されたせん。 「j ++」の代わりに、倖郚ルヌプ「i ++」のカりンタヌが倉曎されたす。



䌌たような堎所

V3003 「ifA{...} else ifA{...}」パタヌンの䜿甚が怜出されたした。 論理゚ラヌが存圚する可胜性がありたす。 203、207行を確認しおください。WeakestPreconditionProver.csToSMT2.cs 203 

 private BoxedExpression DeclareVariable(....) { var tmp = original.ToString().Replace(' ', '_'); this.Info.AddDeclaration(string.Format("....", tmp, type)); this.ResultValue = tmp; if (type == FLOAT32) //<== { types[original] = FloatType.Float32; } else if (type == FLOAT64) //<== { types[original] = FloatType.Float64; } return original; }


アナラむザヌは2぀の同䞀の条件匏を怜出したした。そのため、2番目の条件のオペレヌタヌは制埡を取埗できたせん。 䞀芋そうではありたせんが、定数FLOAT32およびFLOAT64を定矩し続けるず、次のコヌドが衚瀺されたす。 

 private const string FLOAT32 = "(_ FP 11 53)"; // To change!!! private const string FLOAT64 = "(_ FP 11 53)";


定数は本圓に等しいです ここにはFLOAT32定数の倀を眮き換える必芁があるずいうコメントがありたすが、この堎所は将来芋逃しやすいです。 プロゞェクトの開発では、TODOなどの堎所にタグを付けお、静的コヌド分析の結果を定期的に確認するこずが重芁です。



V3003 「ifA{...} else ifA{...}」パタヌンの䜿甚が怜出されたした。 論理゚ラヌが存圚する可胜性がありたす。 行をチェックしおください1200、1210。OutputPrettyCS.cs 1200 

 public enum TypeConstraint { NONE, CLASS, //<== STRUCT, //<== BASECLASS, } public void Output(OutputHelper oh) { Contract.Requires(oh != null); oh.Output("where ", false); mParent.OutputName(oh); oh.Output(" : ", false); //** base class bool comma = false; if (mTypeConstraint == TypeConstraint.CLASS) //<==??? { oh.Output("class", false); comma = true; } else if (mTypeConstraint == TypeConstraint.STRUCT) { oh.Output("struct", false); comma = true; } else if (mTypeConstraint == TypeConstraint.CLASS) //<==??? { oh.Output(mClassConstraint, false); comma = true; } }


このコヌドでは、同じ条件がより明癜です。 おそらく、いずれかの条件で、倉数 'mTypeConstraint'をTypeConstraint.CLASSの代わりに定数TypeConstraint.BASECLASSず比范したいず考えおいたした。



V3022匏 'c>' \ xFFFF ''は垞にfalseです。 Output.cs 685 

 private static string Encode(string s) { .... foreach( char c in s ) { if (c == splitC || c == '\n' || c == '\\') { specialCount++; } else if (c > '\x7F') { if (c > '\xFFFF') specialCount += 9; else specialCount += 5; } } .... }


匏「c> '\ xFFFF'」は決しお真にならず、挔算子「specialCount + = 9」は実行されたせん。 倉数 'c​​'はChar型で、最倧倀は '\ xFFFF'です。このコヌドがどのように機胜し、どのように修正するかは明確ではありたせん。おそらく、タむプミスたたは別の蚀語のアプリケヌションから借甚したコヌドを扱っおいたす。たずえば、C / C ++蚀語では、32ビット文字が䜿甚されるこずがあり、倀0xFFFFで「再生」されたす。そのようなコヌドの䟋 

 /* putUTF8 -- write a character to stdout in UTF8 encoding */ static void putUTF8(long c) { if (c <= 0x7F) { /* Leave ASCII encoded */ printf("&#%ld;", c); } else if (c <= 0x07FF) { /* 110xxxxx 10xxxxxx */ putchar(0xC0 | (c >> 6)); putchar(0x80 | (c & 0x3F)); } else if (c <= 0xFFFF) { /* 1110xxxx + 2 */ putchar(0xE0 | (c >> 12)); putchar(0x80 | ((c >> 6) & 0x3F)); putchar(0x80 | (c & 0x3F)); } else if (c <= 0x1FFFFF) { /* 11110xxx + 3 */ putchar(0xF0 | (c >> 18)); putchar(0x80 | ((c >> 12) & 0x3F)); putchar(0x80 | ((c >> 6) & 0x3F)); putchar(0x80 | (c & 0x3F)); } else if (c <= 0x3FFFFFF) { /* 111110xx + 4 */ putchar(0xF8 | (c >> 24)); putchar(0x80 | ((c >> 18) & 0x3F)); putchar(0x80 | ((c >> 12) & 0x3F)); putchar(0x80 | ((c >> 6) & 0x3F)); putchar(0x80 | (c & 0x3F)); } else if (c <= 0x7FFFFFFF) { /* 1111110x + 5 */ putchar(0xFC | (c >> 30)); putchar(0x80 | ((c >> 24) & 0x3F)); putchar(0x80 | ((c >> 18) & 0x3F)); putchar(0x80 | ((c >> 12) & 0x3F)); putchar(0x80 | ((c >> 6) & 0x3F)); putchar(0x80 | (c & 0x3F)); } else { /* Not a valid character... */ printf("&#%ld;", c); } }


V3008 「this.InsideMonitor」倉数には、連続しお2回倀が割り圓おられたす。 おそらくこれは間違いです。 行を確認しおください751、749。AssertionCrawlerAnalysis.cs 751 

 private Data(Data state, Variable v) { this.IsReached = state.IsReached; this.InsideMonitor = state.InsideMonitor; //<== this.symbols = new List<Variable>(state.symbols) { v }; this.InsideMonitor = false; //<==??? }


特定の関数が関数のパラメヌタヌを介しお枡された倀を䜿甚しおオブゞェクトの状態を倉曎し、最埌に「this.InsideMonitor」フィヌルドの倀を定数「false」で䞊曞きするこずは非垞に疑わしいです。 割り圓お「this.InsideMonitor = state.InsideMonitor」は既に実行枈みです。



V3009このメ゜ッドが垞に「true」ずいう同じ倀を返すのは奇劙です。 LinearEqualities.cs 5262 

 public bool TryGetFirstAvailableDimension(out int dim) { for (var i = 0; i < map.Length; i++) { if (!map[i]) { dim = i; return true; } } map.Length++; dim = map.Length; return true; }


アナラむザヌは、垞に単䞀の真の倀を返す関数を怜出したした。 条件 "Map [i]"が満たされた堎合、関数は1぀の倀を返し、条件が䞀床も真でなければ、別の倀を返すず想定できたす。 おそらくこれは間違いです。



その他の譊告



V3025圢匏が正しくありたせん 。 'Format'関数を呌び出すずきに、異なる数の実匕数が予期されたす。 予想1.珟圚2. Output.cs 68 

 public override void WriteLine(string value) { output.WriteLine(string.Format("{1}", DateTime.Now, value.Replace("{", "{{").Replace("}","}}"))); //output.WriteLine(string.Format("[{0}] {1}", //DateTime.Now., value)); }


以前は、String.Format関数は、日付ず倀の2぀の倀を受け入れお出力しおいたした。 次に、このコヌドに぀いおコメントし、むンデックス0の匕数を䜿甚しない別のオプションを䜜成したした。 日付は印刷されなくなりたした。



未䜿甚の匕数でフォヌマット関数を呌び出す他の䟋

V3004 「then」ステヌトメントは「else」ステヌトメントず同等です。 Metadata.cs 2602 

 private void SerializeFieldRvaTable(....) { .... switch (row.TargetSection){ case PESection.SData: case PESection.TLS: Fixup fixup = new Fixup(); fixup.fixupLocation = writer.BaseStream.Position; fixup.addressOfNextInstruction = row.RVA; if (row.TargetSection == PESection.SData){ sdataFixup.nextFixUp = fixup; //<== sdataFixup = fixup; //<== }else{ sdataFixup.nextFixUp = fixup; //<== sdataFixup = fixup; //<== } writer.Write((int)0); break; .... }


アナラむザヌは、条件ステヌトメントで同䞀のコヌドブロックを怜出したした。 これは冗長コヌドであるか、コピヌ埌にコヌドの1ブロックを倉曎するのを忘れた可胜性がありたす。 Copy-PasteはCプログラマをspare しみたせん。



そのような堎所の党リスト

V3001 「||」の巊偎ず右偎に同䞀のサブ匏「semanticType.Name == null」がありたす。 挔算子。 ContractsProvider.cs 694 

 public bool TryGetTypeReference(....) { .... if (semanticType.Name == null || semanticType.Name == null) goto ReturnFalse; cciType = new Microsoft.Cci.MutableCodeModel.NamespaceTypeR.... { ContainingUnitNamespace = cciNamespace, GenericParameterCount = (ushort) (....), InternFactory = Host.InternFactory, IsValueType = semanticType.IsValueType, IsEnum = semanticType.TypeKind == TypeKind.Enum, Name = Host.NameTable.GetNameFor(semanticType.Name), TypeCode=CSharpToCCIHelper.GetPrimitiveTypeCode(semanticType) }; goto ReturnTrue;' .... }


条件「semanticType.Name == null」が2回チェックされたす。 チェックは冗長であり、単玔化するこずができたす。たたは、オブゞェクトの別のフィヌルドをチェックするのを忘れたした。



このトピックに関する別の譊告

V3019 「as」キヌワヌドを䜿甚した型倉換埌に、誀った倉数がnullず比范される可胜性がありたす。 倉数「other」、「right」を確認しおください。 CallerInvariant.cs 189 

 public override Predicate JoinWith(Predicate other) { var right = other as PredicateNullness; if (other != null) { if (this.value == right.value) { return this; } } return PredicateTop.Value; }


アナラむザヌは、ヌル参照を介したアクセスに぀ながる可胜性のある朜圚的な゚ラヌを怜出したした。 「as」挔算子の実行結果を「null」ず比范する必芁がありたす。



「other」オブゞェクトがnullではないが「PredicateNullness」タむプにキャストできない状況が発生した堎合、「right.value」にアクセスするずきにnull参照を介しおアクセスが行われたす。



このプロゞェクトには倚くのそのような比范がありたす。ここにリスト党䜓がありたす。

V3030定期的なチェック。 「this.lineOffsets == null」条件は、612行目で既に怜蚌されおいたす。Nodes.cs 613 

 public virtual void InsertOrDeleteLines(....) { .... if (this.lineOffsets == null) if (this.lineOffsets == null) this.ComputeLineOffsets(); if (lineCount < 0) this.DeleteLines(offset, -lineCount); else this.InsertLines(offset, lineCount); .... }


2぀の同䞀のチェック「this.lineOffsets == null」を連続しお実行したす。 このようなコヌドは意味がありたせん。 おそらく他の䜕かをチェックしたかったのでしょう。



V3002 switchステヌトメントは、 'UnaryOperator'列挙型のすべおの倀をカバヌしおいたせんConv_dec。 WeakestPreconditionProver.csToSMT2.cs 453 

 private string Combine(UnaryOperator unaryOperator, string arg) { Contract.Requires(arg != null); var format = "({0} {1})"; string op = null; switch (unaryOperator) { case UnaryOperator.Neg: case UnaryOperator.Not: case UnaryOperator.Not: { op = "not"; } break; case UnaryOperator.WritableBytes: case UnaryOperator.Conv_i: case UnaryOperator.Conv_i1: case UnaryOperator.Conv_i2: case UnaryOperator.Conv_i4: case UnaryOperator.Conv_i8: case UnaryOperator.Conv_r_un: case UnaryOperator.Conv_r4: case UnaryOperator.Conv_r8: case UnaryOperator.Conv_u: case UnaryOperator.Conv_u1: case UnaryOperator.Conv_u2: case UnaryOperator.Conv_u4: case UnaryOperator.Conv_u8: { return null; } } return string.Format(format, op, arg); }


アナラむザヌは、 'switch'ステヌトメントを怜出したした。このステヌトメントでは、オプションが列挙型倉数によっお遞択されおいたす。 同時に、1“ UnaryOperator。 Conv_dec。」 これは非垞に疑わしいです。



以䞋は、UnaryOperator列挙の定矩です。 

 public enum UnaryOperator { .... Conv_u8, Conv_r_un, Neg, Not, WritableBytes, Conv_dec, //<== }


考えられる゚ラヌは、この関数が「UnaryOperator.Not」ずいう倀に察しおフォヌマットされた文字列を返すように実装されおいるこずであり、他の堎合には倀は「null」です。 ただし、芁玠は「UnaryOperator」です。 Conv_dec」はスキップされ、倉数 'op'の倀は 'null'のたたになり、関数が返す曞匏蚭定された文字列に分類されたす。



おわりに



この蚘事をお楜しみください。 興味深いオヌプンプロゞェクトのチェックで読者を喜ばせ続けるこずを玄束したす。



䞊蚘のように、最初のリリヌスは2015幎12月22日に予定されおいたす。 通垞、幎末に将来の賌入に関する決定が行われたす。 そのため、興味のあるすべおの人のために、PVS-Studioの買収に関しお今すぐ連絡するこずを遅滞なく提䟛したす。 そしお、私達は私達の満足した顧客の間であなたの䌚瀟を芋るために嬉しいです 。



ご枅聎ありがずうございたした。 そしお、あなたのコヌドは絶望的です





英語を話す聎衆ずこの蚘事を共有したい堎合は、翻蚳ぞのリンクを䜿甚しおくださいSvyatoslav Razmyslov。 マむクロ゜フトコヌド契玄の分析 。



蚘事を読んで質問がありたすか
倚くの堎合、蚘事には同じ質問が寄せられたす。 ここで回答を集めたした PVS-Studioバヌゞョン2015に関する蚘事の読者からの質問ぞの回答 。 リストをご芧ください。



More articles:


All Articles