vermaseren / form

The FORM project for symbolic manipulation of very big expressions
GNU General Public License v3.0
1.16k stars 138 forks source link

id all, nested functions, argument field wildcards #122

Open tueda opened 8 years ago

tueda commented 8 years ago

The following FORM code crashes:

S x1,...,x9;
CF f,g;
L F = f(g(x1,x2),g(x3,x4));
id all, f(g(?a,x1?,?b),g(?c)) = f(g(?a,?b),g(?c)) * g(x1);
P +s;
.end

Valgrind output:

==17502== 
FORM 4.1 (Aug 30 2016, v4.1-20131025-242-g897eab2) 64-bits  Run: Wed Aug 31 15:43:10 2016
    S x1,...,x9;
    CF f,g;
    L F = f(g(x1,x2),g(x3,x4));
    id all, f(g(?a,x1?,?b),g(?c)) = f(g(?a,?b),g(?c)) * g(x1);
    P +s;
    .end
==17502== Invalid read of size 8
==17502==    at 0x47E8C7: SubsInAll (pattern.c:2068)
==17502==    by 0x443330: ScanFunctions (function.c:1897)
==17502==    by 0x43EC57: FindRest (findpat.c:1133)
==17502==    by 0x442077: MatchFunction (function.c:1432)
==17502==    by 0x442DF5: ScanFunctions (function.c:1771)
==17502==    by 0x43EC57: FindRest (findpat.c:1133)
==17502==    by 0x47F9CA: TestMatch (pattern.c:533)
==17502==    by 0x4B53A0: Generator (proces.c:3598)
==17502==    by 0x4B5644: Generator (proces.c:3668)
==17502==    by 0x4B5644: Generator (proces.c:3668)
==17502==    by 0x4B5A53: Generator (proces.c:3836)
==17502==    by 0x4B6FB0: Processor (proces.c:404)
==17502==  Address 0x5603d98 is 8 bytes before a block of size 800 alloc'd
==17502==    at 0x4A06A2E: malloc (vg_replace_malloc.c:270)
==17502==    by 0x4FA592: Malloc1 (tools.c:2214)
==17502==    by 0x42B383: inicbufs (comtool.c:60)
==17502==    by 0x4E1BEB: StartVariables (startup.c:963)
==17502==    by 0x4E3A7B: main (startup.c:1525)
==17502== 
==17502== Invalid read of size 4
==17502==    at 0x42AA85: AddNtoC (comtool.c:271)
==17502==    by 0x47E908: SubsInAll (pattern.c:2077)
==17502==    by 0x443330: ScanFunctions (function.c:1897)
==17502==    by 0x43EC57: FindRest (findpat.c:1133)
==17502==    by 0x442077: MatchFunction (function.c:1432)
==17502==    by 0x442DF5: ScanFunctions (function.c:1771)
==17502==    by 0x43EC57: FindRest (findpat.c:1133)
==17502==    by 0x47F9CA: TestMatch (pattern.c:533)
==17502==    by 0x4B53A0: Generator (proces.c:3598)
==17502==    by 0x4B5644: Generator (proces.c:3668)
==17502==    by 0x4B5644: Generator (proces.c:3668)
==17502==    by 0x4B5A53: Generator (proces.c:3836)
==17502==  Address 0x0 is not stack'd, malloc'd or (recently) free'd
==17502== 
Program terminating at 1.frm Line 5 --> 
==17502== Invalid read of size 4
==17502==    at 0x4FD34D: Crash (tools.c:3541)
==17502==    by 0x4E331A: Terminate (startup.c:1683)
==17502==    by 0x4E3A26: onErrSig (startup.c:1452)
==17502==    by 0x3A4983265F: ??? (in /lib64/libc-2.12.so)
==17502==    by 0x42AA84: AddNtoC (comtool.c:269)
==17502==    by 0x47E908: SubsInAll (pattern.c:2077)
==17502==    by 0x443330: ScanFunctions (function.c:1897)
==17502==    by 0x43EC57: FindRest (findpat.c:1133)
==17502==    by 0x442077: MatchFunction (function.c:1432)
==17502==    by 0x442DF5: ScanFunctions (function.c:1771)
==17502==    by 0x43EC57: FindRest (findpat.c:1133)
==17502==    by 0x47F9CA: TestMatch (pattern.c:533)
==17502==  Address 0x0 is not stack'd, malloc'd or (recently) free'd
tueda commented 8 years ago

Another example to crash, in which argument field wildcards are contained in a bit different way:

CF f,R;
S x1,x2,x3;
L F = f(R(1,2)) * R(3);
id all, f(?a,R(x1?,x2?),?b) * R(x3?) = f(x1,x2,x3);
.end
vermaseren commented 8 years ago

This is rather complicated. The way the backtracking works, the normal matches abort after success. In the case of id,all the program stores the complete match and continues. This cannot work well when multiple matches could occur inside functions inside functions, because when it has the match inside the deepest function, it returns to one level lower and keeps looking for the remaining part of the pattern. There is no way to return later to the point in the deepest function to continue there (at least not at the moment). As it was, it had the match inside the deepest function and thought it could complete things there, even though other wildcards had not been assigned yet. This caused the crash or other wild behaviour. I have now made it such that it only keeps looking for more matches to one level deep as in ` S x1,...,x9; CF f,g; L F = f(g(x1,x2),g(x3,x4)); id,all,f(?a,g(?b,x1?,?c),?d) = f(?a,g(?b,?c),?d)*g(x1); P +s; .end

F =

As you see, at the first level it can keep going; at the second level it cannot. I do not know yet how to make it work properly at higher levels without having to make massive changes.

Jos