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