forked from cil-project/cil
-
Notifications
You must be signed in to change notification settings - Fork 0
/
NOTES
86 lines (59 loc) · 3.14 KB
/
NOTES
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
81
82
83
84
85
86
TODO list
CIL
------
Front-end
- trigraph sequences (??:, ...) ISO 5.2.1.1
- name spaces for struct/enum/union are the same ISO 6.2.3
- check integer conversion ISO 6.3.1.1
- character constants (type, value, escapes) ISO 6.4.4.4
- string literals (value, escapes) ISO 6.4.5
- punctuation tokens ISO 6.4.6
- default argument promotions in function calls ISO 6.5.2.2
- compound literals ISO 6.5.2.5. Missing fields initialized to 0!!
- check that long long is properly done in type specs ISO 6.7.2
- Initialization ISO 6.7.8
- MSVC has a bug in the handling of shift operators: arithemtic conversions
are applies on both operands instead of just integral promotions. We duplicate
this bug in doBinOp in cabs2cil.
- we should allow the user to specify a logging function that takes
printf()-style arguments (rather than hardcoding syslog/printk/printf).
- the restrict attribute is dropped in cabs2cil
- struct and union must share the name space
- when merging we use too much memory. We should be droping the references to
the CABS files once we convert each one to CIL.
CCURED
==============
- if we use memcpy to copy some stuff from local variables to the heap we
might be moving stack pointers that way. The only way to prevent that is to
disallow storing stack pointers in local variables that are arrays or whose
address is taken.
- in box.ml offsetOfFirstScalar looks only at the first field of a union.
- in box.ml when we check tags we check all fields in a union. This is sound
but excessive.
(2) Make a file with global declarations of common functions like strcpy().
These declarations should include pointer annotations and should be
used instead of the ones that appear in the source.
?(9) Find some way to describe [recursive] types at runtime and use them as
tags.
- on MSVC we turn on 32-bit packing of stuff
- Writing or reading unaligned pointers is not allowed.
- Right now when we try to read a pointer and we don't find one in tags, we
overwrite the base part of the pointer to be read with 0. But this might
have undesired side-effects.
- I wonder what do we do when casting between abstract types (struct foo *
where struct foo is not defined)
- change CHECK_RETURNPTR and CHECK_STOREPTR so that the range checked
is 512K (instead of 1 meg) for Linux Kernel Drivers.
- add a flag that effectively puts #pragma box(off) / #pragma box(on)
around all global initializers in a file.
- turning interface char* into ROSTRING is unsound. This is done even when
the item is subject to writes.
- printf is not quite safe. If we do not manage to verify statically the
arguments we should be calling a wrapper. Do we do that?
- in a SEQ pointer we must keep the end = null if the poiner is an integer.
Else there is trouble when we cast to FSEQ. Can we cast integers into FSEQ?
- sm: because wild area lengths have word-level granularity, we can't protect
the final 0 of a char array unless the alignment works out; solutions
include changing granularity to bytes (painful) or changing the array-
expander to ensure alignment (potentially wasteful of a few bytes here
and there)