- A Concurrent Affair - https://www.concurrentaffair.org -

Generalized Method Argument Arrays and XML

Today I finished generalizing the annotations that pass method arguments as arrays and provide OnlySynchronizedArgument, NotSynchronizedArgument, OnlyNullArgument, NotNullArgument annotations, and perhaps something more unusual, NumberBoundedArgument, along with the matching Any, All and None combinations.

Just like all the annotations named above, NumberBoundedArgument lets you specify the index of the argument you want checked, and then it lets you select several modes:

where arg is the argument being compared, bound is one of the bounds(either the upper bound for LESS, LESS\_EQ, IN, and IN\_EQ; or upper bound for GREATER and GREATER\_EQ), and upperBound is the upper bound for IN, IN\_EQ, GREATER and GREATER\_EQ.

I decided to use bound both as upper and lower bound for those annotations that only use one bound as that was less confusing. Otherwise, I’d have to remember whether I set ubound or lbound for LESS.

I have also finished XML importing and exporting so that it supports passing arguments, and I fixed a bug that didn’t properly join predicate annotations if the invariant was repeated several times.

I also improved violation reporting: If method arguments are passed, then the actual values will also appear in the violation log.

Consider the following nice program that uses NumberBoundedArgument:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
package sample.threadCheck.predicate;
import edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument;
public class TCSample17 {
    public static void main(String [1][] args) {
        TCSample17 o = new TCSample17();
        System [2].out.println("main!");
        o.succeeds();
        o.fails();
        System [2].out.println("end main!");
    }

    void succeeds() { // these invariants all succeed
        lt(0); ltEq(0);
        gt(0); gtEq(0);
        in(0); inEx(0);
        out(0); outEx(3);
    }

    void fails() { // these invariants all fail
        lt(2); ltEq(2);
        gt(-1); gtEq(-2);
        in(1); inEx(1);
        out(2); outEx(0);
    }

    @NumberBoundedArgument(
      mode=NumberBoundedArgument.Mode.LESS,
      index = 0, bound = 1)
    void lt(int i) {
        System [2].out.println("lt, i = "+i);
    }

    @NumberBoundedArgument(
      mode=NumberBoundedArgument.Mode.LESS\_EQ,
      index = 0, bound = 0)
    void ltEq(int i) {
        System [2].out.println("ltEq, i = "+i);
    }

    @NumberBoundedArgument(mode=NumberBoundedArgument.Mode.GREATER,
      index = 0,
      bound = -1)
    void gt(int i) {
        System [2].out.println("gt, i = "+i);
    }

    @NumberBoundedArgument(
      mode=NumberBoundedArgument.Mode.GREATER\_EQ,
      index = 0, bound = 0)
    void gtEq(int i) {
        System [2].out.println("gtEq, i = "+i);
    }

    @NumberBoundedArgument(
      mode=NumberBoundedArgument.Mode.IN\_EQ,
      index = 0, bound = 0, upperBound = 0)
    void in(int i) {
        System [2].out.println("in, i = "+i);
    }

    @NumberBoundedArgument(
      mode=NumberBoundedArgument.Mode.IN,
      index = 0, bound = -1, upperBound = 1)
    void inEx(int i) {
        System [2].out.println("inEx, i = "+i);
    }

    @NumberBoundedArgument(
      mode=NumberBoundedArgument.Mode.OUT\_EQ,
      index = 0, bound = 1, upperBound = 3)
    void out(int i) {
        System [2].out.println("out, i = "+i);
    }

    @NumberBoundedArgument(mode=NumberBoundedArgument.Mode.OUT,
      index = 0, bound = 0, upperBound = 2)
    void outEx(int i) {
        System [2].out.println("outEx, i = "+i);
    }
}

When executed, it produces the following log file:

========================================
Log opened 2007-03-05, 02:44:17 CST (GMT-5)
----------------------------------------
Thread Predicate Violation: (9 checks, 1 violation)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.lt (TCSample17.java:43)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:31)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (10 checks, 2 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.ltEq (TCSample17.java:48)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:32)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (11 checks, 3 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'-1' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.gt (TCSample17.java:53)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:33)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (12 checks, 4 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'-2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.gtEq (TCSample17.java:58)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:34)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (13 checks, 5 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'1' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.in (TCSample17.java:63)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:35)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (14 checks, 6 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'1' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.inEx (TCSample17.java:68)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:36)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (15 checks, 7 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'2' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.out (TCSample17.java:73)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:37)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)
----------------------------------------
Thread Predicate Violation: (16 checks, 8 violations)
	Current thread 'main', id 1, group 'main'
	Violated predicate @edu.rice.cs.cunit.threadCheck.predicates.NumberBoundedArgument
	Method arguments
		'0' : java.lang.Integer
	at sample.threadCheck.predicate.TCSample17.outEx (TCSample17.java:78)
	at sample.threadCheck.predicate.TCSample17.fails (TCSample17.java:38)
	at sample.threadCheck.predicate.TCSample17.main (TCSample17.java:13)

This is a lot more informative than it used to be.

[3] [4]Share [5]