Geekly Articles each Day
📜 ⬆️ ⬇️

Checking Microsoft Code Contracts



We have successfully created and continue to develop the PVS-Studio analyzer for the C / C ++ language. Over time, it became clear that many of the implemented diagnostics are in no way associated with a specific programming language, and then we decided to try to apply our experience to another programming language, to C #. This article will discuss the verification of the Microsoft Code Contracts project using a new C # analyzer.

About MS Code Contracts


Code Contracts provide a method by which assumptions about program code in .NET applications are expressed. Contracts take the form of preconditions, postconditions, and invariants of an object, and act as verified documentation of your external and internal APIs. Contracts are used to improve the testing process through verification during program execution, allowing for static verification of contracts and the generation of documentation.

This is a medium-sized project (about ~ 4,000 source files) that is being actively developed: it contains a lot of unfinished and incorrectly written code. It is at this stage that it is necessary to introduce static analysis into the development process.
')

About the new C # code analyzer


The Code Contracts project was tested using the experimental version of PVS-Studio , which is available at this link: http://files.viva64.com/beta/PVS-Studio_setup.exe .

The analyzer will soon cease to be experimental. We are planning to release the first release version of PVS-Studio with C # support already 12/22/2015. In this case, the analyzer changes the major version number to 6.0.

Pricing policy will not undergo any changes. Previously, PVS-Studio allowed you to check programs in C, C ++, C ++ / CLI, C ++ / CX. Now C # is simply added to this list.

Test results


Preparing an article about checking an open project , we provide in it information far from all warnings issued by the static analyzer. Therefore, we recommend that project authors independently perform project analysis and study all messages issued by the analyzer.

The most dangerous places found


V3025 Incorrect format. A different number of actual arguments is expected while calling 'Format' function. Expected: 3. Present: 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 )); .... }

The function String.Format () expects 3 arguments, and only 2 arguments are passed. In this case, a FormatException occurs.

V3014 It is likely that a variable is being incremented inside the 'for' operator. Consider reviewing '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(); }

In a nested loop, the 'j' counter variable does not change, since instead of 'j ++', the counter of the outer loop 'i ++' is changed.

Some more similar places:
V3003 The use of if (A) {...} else if (A) {...} 'pattern was detected. There is a possibility of logical error presence. Check lines: 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; }

The analyzer detected two identical conditional expressions, which is why the operators in the second condition will never get control. Although, at first glance, this is not the case, we will proceed to the definition of the constants FLOAT32 and FLOAT64, and we will see the following code:
 private const string FLOAT32 = "(_ FP 11 53)"; // To change!!! private const string FLOAT64 = "(_ FP 11 53)";

Constants are really equal! Although there is a comment here that it is necessary to replace the value of the constant FLOAT32, this place is easy to miss in the future. In developing projects, it is important to mark places like TODO and regularly review the results of static code analysis.

V3003 The use of if (A) {...} else if (A) {...} 'pattern was detected. There is a possibility of logical error presence. Check lines: 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; } }

In this code snippet, the same conditions are more obvious. Most likely, in one of the conditions, the 'mTypeConstraint' variable was wanted to be compared with the TypeConstraint.BASECLASS constant, instead of TypeConstraint.CLASS.

V3022 Expression 'c>' \ xFFFF '' is always 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; } } .... }

The expression “c> '\ xFFFF'” will never be true and the “specialCount + = 9” operator will never be executed. The variable 'c' is of type Char, the maximum value of which is '\ xFFFF'. It is not very clear how this code should work and how it should be corrected. Perhaps we are dealing with a typo or code fragment borrowed from an application in another language. For example, in the C / C ++ language, sometimes 32-bit characters are used, and there they just "play" with the value 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 The 'this. InsideMonitor' variable is assigned values ​​twice successively. Perhaps this is a mistake. Check lines: 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; //<==??? }

It is very suspicious that a certain function changes the state of an object using the values ​​passed through the parameters of the function and at the last moment overwrites the value of the “this.InsideMonitor” field with the constant 'false'. The assignment "this.InsideMonitor = state.InsideMonitor" has already been made.

V3009 It's one of those true values. 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; }

The analyzer has detected a function that always returns one true value. It can be assumed that if the condition "! Map [i]" is fulfilled, the function should return one value, and if the condition was never true, then return another value. Perhaps there is a mistake.

The remaining warnings


V3025 Incorrect format. A different number of actual arguments is expected while calling 'Format' function. Expected: 1. Present: 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)); }

Previously, the String.Format () function accepted and printed 2 values: a date and some value. Then this code was commented out and another variant was written, in which the argument with index 0 is not used, i.e. The date is now not printed.

Other examples of calling formatting functions with unused arguments:
V3004 The 'then' statement is equivalent to the 'else' statement. 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; .... }

The analyzer detected identical code blocks in a conditional statement. This may be an extra code or one block of code forgot to change after copying. Copy-Paste does not spare C # programmers.

All list of similar places:
V3001 There are identical sub-expressions' semanticType.Name == null '||' operator. 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;' .... }

The condition "semanticType.Name == null" is checked 2 times. Either the check is redundant and it can be simplified, or forgot to check another field of the object.

Another warning on this topic:
V3019 Possibly incorrectly variable conversion compared to null after type conversion using 'as' keyword. Check variables '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; }

The analyzer has detected a potential error that may lead to access via a null link. It is necessary to compare with 'null' the result of the 'as' statement.

If a situation arises when the object 'other' is not zero, but it cannot be converted to the type 'PredicateNullness', then access will be made to the zero reference when accessing “right.value”.

Many such comparisons have been found in the project, here’s the entire list:
V3030 Recurring check. The 'this.lineOffsets == null' condition was already verified in line 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); .... }

Two consecutive identical checks “this.lineOffsets == null”. Such code does not make sense. Perhaps they wanted to check something else.

V3002 Enum : 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); }

The analyzer detected the 'switch' operator, in which the choice of a variant is carried out according to the enum-type variable. In this case, in the switch statement, 1 element “UnaryOperator is missing. Conv_dec. This is very suspicious.

The following is the definition of the UnaryOperator enumeration:
 public enum UnaryOperator { .... Conv_u8, Conv_r_un, Neg, Not, WritableBytes, Conv_dec, //<== }

A possible error is that this function is implemented in such a way that for the value “UnaryOperator. Not” to return a formatted string, and in other cases the value is 'null'. But since the element is “UnaryOperator. Conv_dec "is omitted, then for it the value of the variable 'op' will remain equal to 'null' and it will fall into the formatted string that the function will return.

Conclusion


We hope you enjoyed this article. We promise to continue to delight our readers with checks of interesting open source projects.

As mentioned above, the first release is scheduled for 12/22/2015. As a rule, at the end of the year decisions are made on future purchases. Therefore, to all those interested, we offer, without delay, to contact us now regarding the purchase of PVS-Studio. And we will be glad to see your company among our satisfied customers .

Thanks for attention. And bezbezhnogo you code!


If you want to share this article with an English-speaking audience, then please use the link to the translation: Svyatoslav Razmyslov. Analysis of Microsoft Code Contracts .

Read the article and have a question?
Often our articles are asked the same questions. We collected answers to them here: Answers to questions from readers of articles about PVS-Studio, version 2015 . Please review the list.

Source: https://habr.com/ru/post/273111/

More articles:


All Articles