Points to improve in points-to analysis No priority order. 8. EffectsWithPointsTo: Also in call14 or call05, probably an interprocedural translation issue in call08 for _x_3 in the callee and y in the caller. Also, many returns are missing in the source codes of EffectsWithPointsTo: they would be useful to debug the points-to analysis 9. EffectsWithPointsTo/call09.c: duplicate effect on s.one. Same in call10. 10. EffectsWithPointsTo/call15.c: understand the "may be written", probably due to NULL pointer initialization, but should have been automatically eliminated by the dereferencement. In fact call15 does not check its argument pi or q. Stricto sensu, it is really a may. But if summary information is linked to a function that returns, the information should be a must at the caller level... See also results for struct22 and probably many other test cases. 11. EffectsWithPointsTo/chap2_exp4: why do we get a maybe effect on *heap*? Because the heap lattice is not precise enough to distinguish between exact heap references and abstract heap references. Add an extra dimension to model the occurences? See below heap modeling (19). 12. EffectsWithPointsTo/dereferencing06: improved results thanks to a better analysis of pointer arithmetics. 13. EffectsWithPointsTo/fpointer01: result is now less precise. 14. EffectsWithPointsTo/fulguro04: result modified to take into account an implicit dimension. 15. EffectsWithPointsTo: differences from global02 to varargs04 to be looked at. 18. dereferencing02: a variable, w, is used uninitialized and this is not detected. And there is a bug for "double * z1=*q++". But another bug is detected first: q++ is not allowed since p points toward a scalar, x. 19. Improve heap model. Add an extra first dimension to model the different intraprocedural dynamic occurences of a malloc? Use a different name for the abstract location but indicate a static conflict as with EQUIVALENCEs in Fortran? See Point 11 too. 20. Pre-decrement and pre-increment are likely to be evaluated twice. See the post case in unary_intrinsic_call_to_points_to_sinks(). No test case yet I'm afraid. 22. Handling of >, >=, <, <= in pointer conditions. No test case yet. Implies that both pointers points toward the same object... 24. The consistency check does not check that arcs starting from a vertex of out-degree strictly greater than 1 must be may arcs. 32. statement01_dec: should we generate a NOWHERE rather than a bottom graph? Should this be a property? Ot it should generate a pointer towards an integer stub... which would make dependence testing maybe more difficult... unless you trust the programmer that integer pointer values do not interact with any properly declared variable. 35. Heap model: malloc can return a NULL pointer. This is not the usual case, but it should be controlled by a property... 38. pointer15: the indices for _t_1 are not properly located. The first subscript should be zero for the implicit dimension. [1][2] should be the second and third subscripts 42. Suggestion by Pierre Jouvelot: do not propagate undefined values. This is not implemented. See Pointers/undefined02.c 43. What happens with unions? 44. Lack of translation for Pointers/bc_inter01.c in call to foo(p1, &p2, q2). Samething for Pointers/formal_parameter01.c. Now mishandled subscript on *HEAP*_l_29. 47. When the returned value is a struct, the return cannot be expressed easily because we have to had all the possible fields to the return value... See Pointers/struct20.c 48. The alphabetical/lexicographic sort of points-to arc seems bugged. See Pointers/Strict_typing.sub/pv_assign03.c. 49. A useless space before a comma in the print-out 50. Pointers/StrictTyping.sub/list03: two different names for the same anywhere: // _ll_1.next -> *ANY_MODULE*:*ANYWHERE*_b0 , MAY // _ll_1.next -> *ANY_MODULE*:*ANYWHERE*_b2 , MAY Next item will be 51. ---------------------------------------------------------- Done: 5. Connexion with effects_with_points_to: improve the points-to precondition or use a more powerful function in effects_with_points_to()? Or both? -> I have enriched the points-to information (not sure yet it is enough) 6. Be able to dereference constant pointers, a.k.a. arrays. See Pointers/array03.c, function foo2. Build a smaller test case. -> new test case array14.c 2. C subscript construct analysis: see fulguro04.c for instance and some others: argv03: char *p = (*argv)[1]; fulguro03 fulguro04: (dat->array)[row] Lv pointer08: t->tree_list[i] = (struct tree*) malloc(sizeof(struct tree)); pointer16: t->tree_list[i] = (struct tree*) malloc(sizeof(struct tree)); ptr_to_array01: (*p)[3] = &a; pv_assign05: s1.b[0] = &j; (?) several occurences pv_assign06: s2->b[0] = &i; struct10: a.p[i] = i; struct13: e.champ[i].p = malloc(10*sizeof(int)); (e.champ)[i].p = malloc(10*sizeof(int)); struct21: simplified version of struct13 struct_parall01: a.p[i] = i; 16. Mixed up indices, for instance in argv03. Also pointer15, struct09 -> seems now OK for argv03. FI: I do not know about the other cases. 1. Serious handling of conditions, starting with equality and disequality; see list06.c (altough this piece of code looks dead wrong...) 3. Convergence detection: current implementation no longer works as it used to 4. Add a new dimension to the graph expansion control: outgoing degree, shown in one of the list functions, the freeing of a list (see list05). 21. Conditional operator: arcs created in "in_t" or "in_t" do not appear in "out". See conditional06. -> fixed with a call to merge_points_to_graphs() -> hopefully, approximations are taken a good care of 26. The consistency check does not check that the set is empty when bottom is true. 29. offset_points_to_cell(): the type should be passed in order to update the proper subscript. See dereferencing08.c 30. address_of01: the code is wrong, but gcc does not provide any warning. Neither does PIPS, but it generates a wrong and meaningless reference to i[1]. 31. arithmetic11: type error. One too many [0] subscript... Core dumps. 37. call14: cast in actual argument not properly processed. We might need new stubs to cope with this. -> fixed in that case by tuning the reference according to the cast; namely, (int *) y is changed in &y[0]; 34. Strict_typing.sub/malloc03: "pt++" is not properly interpreted because the sink is not large enough. -> either sources with this issue were modified and the necessary dimension declared or the their tpips were modified to avoid core dumping when a user error is encountered 33. cast must be exploited to avoid further bugs when pointer arithmetic is used. -> at least, partly implemented in simple cases 28. pv_local_var03: issue with declaration and assignment of array of structs; the generated arcs do not seem added to the current "in" points-to environment; it is not clear if index * should or not susbsumes indices 0 and 1. The test case is not good because the rhs struct are not initialized, hence only exact nowhere information is propagated. -> arcs due to local variables do not have to appear in the "in" points-to environment 17. Take care of casts. See for instance Strict_typing.sub/malloc03.c -> a first cut 36. Condition with side effects in and_operator02 is not taken into account. -> not really useful, I believe (FI), but apparently easy to implement. 40. Rice/test03: when the points-to information is recomputed the formal context should be cleaned up, unless it is explictly defined as an input. Samething for the heap. Which means that this stubs should be added to the declaration list of the module... Impact on symbol table? See 41. 41. Rice/test03: the type of entities in the formal context should not be changed once they have been allocated. Unless some code transformation has indeed changed them. For instance, dependent types may be changed into constant types by "partial eval". See 40. -> the past stubs are now deleted before the code is analyzed again after a code transformation, e.g. a constant propagation transforming dependent types into constant types. 27. In Strict_typing.sub/list02, in "main", the points-to obtained on exit of the while loop is declared "unreachable". Same in list03. -> Not observed any more. No idea about the reason. 23. When iterating the analysis of a loop, the points-to graph are accumulated when they should be merged. The accumulation does not update the approximations. See Strict_typing.sub/linked_list01.c for instance. -> Not observed anymore. 25. Strict_typing.sub/fabien03: bug detected by or in a type check. -> fabien03.c fixed; a user warning added before the fatal PIPS error, waiting for more experience with this test... 39. If a stub is added to deal with casts, Rice/test03.c could be parallelized by trusting the type of the pointer "toto". EffectWithPointsTo should also be able to understand these stubs of a new kind... -> up to now, stubs for casts do not appear necessary; test03.c was mishandled for another reason: the type used was changed by a program transformation 46. Returned value not used in Pointers/malloc11.c when "foo" is called in "main". -> Before calling expression_to_points_to_sinks(), expression_to_points_to() must be called first. Bug fix in declaration_statement_to_points_to(). 45. Return value not exploited in Pointers/pointer_free.c -> Bug due to a typedef. The result is still not satisfying because the freed cell is not returned by the analysis. You could think that pointer value could do better. Probably, but I believe that the real reason is that points-to transformer should include a list of freed cells. This should be easy to detect from the equations used to model the impact of a free. 7. EffectsWithPointsTo: the fully subscripted sources and sinks require index substitution in EffectsWithPointsTo, or the parallelism detection is lost; also it is not clear if you want to preserver x[j] instead of *(x+j)....; see for instance call05.c. See also call14.c.