SPARC/ERC32 example: source file exa.adb

  1  -- Example Ada/ERC32 program for Bound-T.
  2  -- Copyright (c) 2006 Tidorum Ltd.
  3  
  4  
  5  procedure Exa is
  6  
  7     type Unsigned_Int is mod 2**32;
  8  
  9  
 10     function Ones (X : Unsigned_Int) return Natural
 11     --
 12     -- Returns the number of '1' bits in X.
 13     -- Demonstrates a "while" loop for which Bound-T cannot find
 14     -- the number of iterations automatically.
 15     --
 16     is
 17  
 18        V : Natural := 0;
 19        -- The number of '1' bits seen so far.
 20  
 21        R : Unsigned_Int := X;
 22        -- The part of X not yet examined.
 23  
 24     begin
 25  
 26        while R /= 0 loop
 27  
 28           if (R and 1) /= 0 then
 29              V := V + 1;
 30           end if;
 31  
 32           R := R / 2;
 33  
 34        end loop;
 35  
 36        return V;
 37  
 38     end Ones;
 39  
 40  
 41     procedure Count25 (X : access Unsigned_Int)
 42     --
 43     -- Demonstrates a loop with static bounds, but a little
 44     -- more complex than a "for" loop.
 45     --
 46     is
 47        U : Integer := 25;
 48        -- The counter.
 49     begin
 50  
 51        while U > 0 loop
 52  
 53           X.all := X.all * Unsigned_Int(U);
 54  
 55           U := U - 2;
 56  
 57        end loop;
 58  
 59     end Count25;
 60  
 61  
 62     procedure Count (
 63        U : in     Integer;
 64        X : access Unsigned_Int)
 65     --
 66     -- Demonstrates a loop that depends on a parameter (U).
 67     --
 68     is
 69        W : Integer := U;
 70        -- A local counter for the loop.
 71     begin
 72  
 73        while W > 0 loop
 74  
 75           X.all := X.all * Unsigned_Int(U);
 76  
 77           W := W - 2;
 78  
 79        end loop;
 80  
 81     end Count;
 82  
 83  
 84     procedure Foo7 (X : access Unsigned_Int) is
 85     --
 86     -- Demonstrates a call to Count with a static value of Count.U
 87     -- that lets Bound-T bound the loop in Count.
 88     --
 89     begin
 90  
 91        X.all := X.all + 10;
 92  
 93        Count (7, X);
 94        -- The loop in Count depends on Count.U = 7.
 95  
 96        X.all := X.all - 8;
 97  
 98     end Foo7;
 99  
100  
101     procedure Foo (
102        Num : in     Integer;
103        X   : access Unsigned_Int) is
104     --
105     -- Demonstrates a call to Count that makes Count.U depend on
106     -- Foo.Num, so that the loop in Count depends on Foo.Num.
107     --
108     begin
109  
110        Count (Num + 3, X);
111  
112     end Foo;
113  
114  
115     procedure Solve (X : access Unsigned_Int)
116     --
117     -- Demonstrates a "for"-loop with static bounds.
118     -- Demonstrates bounding a call (on Count) with assertions.
119     --
120     is
121        K : Integer;
122        pragma Volatile (K);
123        -- To make sure that K is mapped to a storage location.
124     begin
125  
126        for I in 0 .. 7 loop
127           -- The bounds (0..7) in this loop are static.
128  
129           K := Ones (X.all);
130           -- K is now the number of '1' bits in X.all.
131           -- This would be quite hard to analyse statically.
132  
133           exit when K = 0;
134  
135           Count (U => K, X => X);
136  
137        end loop;
138  
139     end Solve;
140  
141  
142     procedure Main
143     --
144     -- Demonstrates calls of various routines.
145     --
146     is
147  
148        X : aliased Unsigned_Int;
149        -- A working variable. Bound-T will not be able to track
150        -- the value of this variable because it is changed in
151        -- the called routines.
152  
153     begin
154  
155        Count25 (X'access);
156        -- This can be bounded automatically because the loop
157        -- in Count25 has static bounds.
158  
159        Foo7 (X'access);
160        -- This can be bounded automatically because Foo7 calls
161        -- Count with a static value for Count.U.
162  
163        Foo (Num => 6, X => X'access);
164        -- This can be bounded automatically because Foo.Num = 6,
165        -- which makes Count.U = 9, which bounds the loop in Count.
166  
167        Solve (X => X'access);
168        -- The loop in Solve can be bounded automatically, but
169        -- not the loop in Count when called from Solve.
170  
171        loop
172           null;
173        end loop;
174        -- This is a simple eternal loop. Bound-T will report it
175        -- and the number of iterations to be included in the WCET
176        -- must be asserted.
177  
178     end Main;
179  
180  
181  begin
182  
183     Main;
184  
185  end Exa;