Commit 4620006
committed
Merge branch 'develop-fix-trigger-arg-arrays'. Close #431.
**Description**
Copilot's C99 backend generates incorrect code. In the generated code,
the functions that generate values passed as arguments to trigger
functions may return pointers to stack-allocated arrays, so the memory
may be used for something else (or freed).
Instead, the structure of the implementation should guarantee that the
arrays are always allocated.
**Type**
- Bug: generated C code may be incorrect.
**Additional context**
- Bug #386 was initially opened for the same reason, but only addressed
the `_gen` functions generated by Copilot. Other functions generated
by Copilot also return pointers to arrays and can fail for the same
reason.
**Requester**
- Ryan Scott (Galois)
**Method to check presence of bug**
The following Dockerfile, and accompanying Copilot and C code, check
that passing a stream of arrays as an argument to a trigger, when
compiled with and without optimizations, produces the same results, in
which case it prints the message Success. The docker image produces a
diff of the two outputs if not:
```
--- Dockerfile-verify-431
FROM ubuntu:trusty
RUN apt-get update
RUN apt-get install --yes software-properties-common
RUN add-apt-repository ppa:hvr/ghc
RUN apt-get update
RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
RUN apt-get install --yes libz-dev
ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
RUN cabal update
RUN cabal v1-sandbox init
RUN cabal v1-install alex happy
RUN apt-get install --yes git
ADD Array.hs /tmp/Array.hs
ADD array_driver.c /tmp/array_driver.c
SHELL ["/bin/bash", "-c"]
CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
&& cabal v1-install $NAME/copilot**/ \
&& cabal v1-exec -- runhaskell /tmp/Array.hs \
&& gcc -O0 /tmp/array_driver.c array.c -I. -o main-no-op && ./main-no-op > no-optimizations \
&& gcc -O /tmp/array_driver.c array.c -I. -o main-op && ./main-op > with-optimizations \
&& diff no-optimizations with-optimizations \
&& echo "Success"
--- Array.hs
{-# LANGUAGE DataKinds #-}
module Main where
import Copilot.Compile.C99
import Language.Copilot
import qualified Prelude as P
spec :: Spec
spec = trigger "f" true [arg stream]
where
stream :: Stream (Array 2 Int16)
stream = constant (array [3,4])
main :: IO ()
main = reify spec >>= compile "array"
--- array_driver.c
#include <stdint.h>
#include <stdio.h>
#include "array_types.h"
#include "array.h"
void f (int16_t f_arg0[(2)]) {
printf("([%d,%d])\n", f_arg0[0], f_arg0[1]);
}
int main(void) {
int i = 0;
printf("f:\n");
for (i=0; i<5; i++) {
step();
}
return 0;
}
```
Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-431
```
**Expected result**
Running the docker image above prints the message success, indicating
that the output structs produced with and without optimizations enabled
are the same.
**Solution implemented**
Modify generated C99 backend so that the output array in a function
producing values passed to triggers as arguments, as well as any they
call that also produces arrays, take the returned array as input. That
way, all memory is preallocated and there's no need for mallocs either
(which we want to avoid).
Identify factorization opportunity for different functions that call
generators and pattern match based on the type of the expression being
generated.
**Further notes**
None.File tree
3 files changed
+36
-31
lines changed- copilot-c99
- src/Copilot/Compile/C99
3 files changed
+36
-31
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | | - | |
| 1 | + | |
2 | 2 | | |
3 | 3 | | |
| 4 | + | |
4 | 5 | | |
5 | 6 | | |
6 | 7 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
163 | 163 | | |
164 | 164 | | |
165 | 165 | | |
| 166 | + | |
| 167 | + | |
| 168 | + | |
| 169 | + | |
| 170 | + | |
| 171 | + | |
| 172 | + | |
| 173 | + | |
| 174 | + | |
| 175 | + | |
166 | 176 | | |
167 | 177 | | |
168 | 178 | | |
169 | 179 | | |
170 | 180 | | |
171 | 181 | | |
172 | 182 | | |
173 | | - | |
174 | | - | |
175 | | - | |
176 | | - | |
| 183 | + | |
177 | 184 | | |
178 | 185 | | |
179 | 186 | | |
| |||
193 | 200 | | |
194 | 201 | | |
195 | 202 | | |
196 | | - | |
197 | 203 | | |
198 | 204 | | |
199 | 205 | | |
| |||
250 | 256 | | |
251 | 257 | | |
252 | 258 | | |
253 | | - | |
254 | | - | |
255 | | - | |
256 | | - | |
257 | | - | |
258 | | - | |
259 | | - | |
260 | | - | |
261 | | - | |
262 | | - | |
263 | | - | |
264 | | - | |
265 | | - | |
266 | | - | |
267 | | - | |
268 | | - | |
| 259 | + | |
| 260 | + | |
269 | 261 | | |
270 | 262 | | |
271 | 263 | | |
| |||
283 | 275 | | |
284 | 276 | | |
285 | 277 | | |
286 | | - | |
| 278 | + | |
287 | 279 | | |
288 | | - | |
289 | | - | |
| 280 | + | |
| 281 | + | |
| 282 | + | |
290 | 283 | | |
291 | | - | |
292 | | - | |
| 284 | + | |
| 285 | + | |
293 | 286 | | |
294 | 287 | | |
295 | 288 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
119 | 119 | | |
120 | 120 | | |
121 | 121 | | |
122 | | - | |
123 | | - | |
124 | | - | |
| 122 | + | |
| 123 | + | |
125 | 124 | | |
126 | 125 | | |
127 | 126 | | |
| |||
130 | 129 | | |
131 | 130 | | |
132 | 131 | | |
133 | | - | |
| 132 | + | |
| 133 | + | |
| 134 | + | |
| 135 | + | |
| 136 | + | |
| 137 | + | |
| 138 | + | |
| 139 | + | |
| 140 | + | |
| 141 | + | |
| 142 | + | |
| 143 | + | |
| 144 | + | |
134 | 145 | | |
135 | 146 | | |
136 | 147 | | |
| |||
0 commit comments