1/*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 */
10
11/*
12 * Type strengthen test cases.
13 */
14
15struct ure {
16  int x;
17  struct ure *n;
18};
19
20
21/*********************
22 * Pure functions.
23 *********************/
24void pure_f(void) {
25}
26
27void pure_f2(void) {
28  pure_f();
29}
30
31struct ure *pure_g(struct ure *p) {
32  return p;
33}
34
35int pure_h(struct ure *p) {
36  return !!p;
37}
38
39int pure_i(int x) {
40  return x;
41}
42
43int pure_j(struct ure s) {
44  return s.x;
45}
46
47int pure_k(struct ure s) {
48  return pure_i(s.x) && pure_j(s);
49}
50
51/* NB: L2Opt removes the division guard, so this lifts successfully. */
52unsigned pure_div_roundup(unsigned x, unsigned n) {
53  /* Quiz: is this function correct? */
54  if(n == 0) return 0;
55  return (x + (n - 1)) / n;
56}
57
58
59
60/*********************
61 * Read-only state monad.
62 *********************/
63unsigned gets_x;
64unsigned gets_y[4];
65
66/*
67   Force the globals to be translated as variables.
68   Otherwise, c-parser turns them into constants because nothing
69   writes to them.
70
71   We could turn on globals_all_addressed in c-parser,
72   but that causes the globals to become generic pointers,
73   and autocorres loses the knowledge that those pointers
74   always point to valid objects.
75
76   Basically, the read-only monad is kind of flimsy and of
77   dubious usefulness. But see type_strengthen_tricks.thy.
78 */
79void hax(void) {
80  gets_x = 42;
81  gets_y[0] = 42;
82}
83
84unsigned gets_f(void) {
85  return gets_x;
86}
87
88unsigned gets_g(void) {
89  unsigned y[4] = {0};
90  y[0] = gets_y[0];
91  y[1] = gets_y[1];
92  y[2] = gets_y[2];
93  y[3] = gets_y[3];
94  if(y[0] && y[1] && y[2] && y[3]) {
95    if(y[0]) y[0] += y[1];
96    if(y[1]) y[1] += y[2];
97    if(y[2]) y[2] += y[3];
98    if(y[3]) y[3] += y[0];
99  } else {
100    y[0] = 1;
101    y[1] += y[0];
102    y[2] += y[1];
103    y[3] += y[2];
104  }
105  return y[0] * y[1] * y[2] * y[3];
106}
107
108
109
110/*********************
111 * Option monad (Read with failure).
112 *********************/
113unsigned opt_f(unsigned *p) {
114  return *p;
115}
116
117int opt_g(int n) {
118  return n + 1;
119}
120
121unsigned opt_h(struct ure *s) {
122  if(!s) return 0;
123  return 1 + opt_h(s->n);
124}
125
126int opt_none(void);
127int opt_i(void) {
128  return opt_none();
129}
130
131int opt_j(struct ure *p, struct ure *l) {
132  return p->x <= l->x;
133}
134
135/* This doesn't read state at all, but AutoCorres assumes loops may fail (to terminate). */
136unsigned opt_l(unsigned n) {
137  unsigned p = 0;
138  while(n > 1) {
139    p++;
140    n /= 10;
141  }
142  return p;
143}
144
145/* Ditto for recursion. */
146unsigned opt_a(unsigned m, unsigned n) {
147  if(m == 0) return n + 1;
148  if(n == 0) return opt_a(m - 1, 1);
149  return opt_a(m - 1, opt_a(m, n - 1));
150}
151
152/* Test for measure_call */
153unsigned opt_a2(unsigned n) {
154  return opt_a(n, n);
155}
156
157
158/*********************
159 * State monad (with failure).
160 * TODO: state monad is no longer used, rename these examples.
161 *********************/
162void st_f(struct ure *p, struct ure *s) {
163  p->n = s;
164}
165
166unsigned st_g(unsigned *p) {
167  *p = 42;
168  return *p;
169}
170
171unsigned st_h(unsigned p) {
172  return st_g((unsigned*)p);
173}
174
175struct ure *st_i(struct ure *p, struct ure *l) {
176  if(opt_j(p, l) || !l) {
177    if(l) {
178      p->n = l->n;
179    }
180    return p;
181  } else {
182    l->n = st_i(p, l->n);
183    return l;
184  }
185}
186
187/*********************
188 * Exception monad, the most general monad.
189 *********************/
190int exc_f(char *s, int *n) {
191  int x = 0;
192  int sg = 1;
193  if(*s == '-') {
194    sg = -1;
195    s++;
196  } else if(*s == '+') {
197    s++;
198  }
199  for(; *s; s++) {
200    if(*s >= '0' && *s <= '9') {
201      x = 10 * x + sg * (*s - '0');
202    } else {
203      return -1;
204    }
205  }
206  if(*s) {
207    return -1;
208  } else {
209    *n = x;
210    return 0;
211  }
212}
213