Closed mariuscrsn closed 3 years ago
GgnDpSngh
commented
3 years ago Hi there,
Thanks for the feedback. I just wanted to check if you are using the latest version? Because the line number 763 in your trace correspond to the "}" statement for me.
Cheers, Gagandeep Singh
mariuscrsn
commented
3 years ago Sorry for the confusion. I added some printf to the file in order to find the bug and I forgot to delete them before running Valgrind. Now I've updated the initial comment with the correct line numbers.
I hope you could find now the bug.
My apologies and thanks again, Marius.
GgnDpSngh
commented
3 years ago Hi Marius,
Thanks for the update. I am unable to locate the problem, however if you could print the following variables after this line (https://github.com/eth-sri/ELINA/blob/20857f8d76005e8579c552068a985f0b16593e3c/elina_poly/opt_pk_assign.c#L302) then that would help me locate the first error. The variables are:
Cheers, Gagandeep Singh
mariuscrsn
commented
3 years ago Hi Gagandeep,
First of all, sorry for taking so long to reply. I have been quite busy the past few days.
In my program the function opt_poly_asssub_linexpr_det is invoked twice.
In the next code, I list the values of the variables that I have printed after the line
https://github.com/eth-sri/ELINA/blob/20857f8d76005e8579c552068a985f0b16593e3c/elina_poly/opt_pk_assign.c#L302
BEGIN opt_poly_asssub_linexpr_det
nbrows: 0
nbvertex: 0
nbline: 1
poly[res]->intdim: 1
BEGIN opt_poly_asssub_linexpr_det
free(): invalid next size (fast)However, in the second invocation, the if condition https://github.com/eth-sri/ELINA/blob/20857f8d76005e8579c552068a985f0b16593e3c/elina_poly/opt_pk_assign.c#L300 that contain this line is not satisfied. So, I can't print the variables you are asking for.
Finally, the program crash on the line https://github.com/eth-sri/ELINA/blob/20857f8d76005e8579c552068a985f0b16593e3c/elina_poly/opt_pk_assign.c#L563
Next, I list the data of poly_a[k] variable that I've printed just before calling this function:
poly_a[k] data:
intdim: 1
realdim: 0
nbeq: 1
nbline: 0
is_minimized: 0
status: 0
C.nbcolumns: 3
C.nbrows: 1
F.nbcolumns: 3
F.nbrows: 1
satC.nbcolumns: 1
satC.nbrows: 1
calling opt_poly_clear(poly_a[k]); ...
free(): invalid next size (fast)If I try to print the nbcolumns and nbrows fields of the satF I get a segmentation fault. So, it could be that the problem is in the matrix allocation.
Thank you for all the effort you are putting into solving the problem.
Regards, Marius.
GgnDpSngh
commented
3 years ago Hi there,
Thanks for the information. I pushed a fix, let me know if the issue is resolved. If not, can you print me the C and F matrix before the crash along with the value of "k" and "num_compa" as well as uncommenting all of he following lines: https://github.com/eth-sri/ELINA/blob/20857f8d76005e8579c552068a985f0b16593e3c/elina_poly/opt_pk_assign.c#L121
Cheers, Gagandeep Singh
mariuscrsn
commented
3 years ago Hi Gagandeep, it is still not working. It continues to crash in the same line as in previous comments. But don't worry, in the upcoming days, I will check my code to make sure that the crash is not caused by my code.
Anyway, I show you the modifications I have made in the code and the output I get.
I list below the body of this for: https://github.com/eth-sri/ELINA/blob/9248e87b9ab2a425ed6fad6f71927aaddfd23f68/elina_poly/opt_pk_assign.c#L561
for(k=0; k < num_compa;k++){
printf("poly_a[k] data for k=%d, num_compa=%d:\n", k, num_compa);
printf("intdim: %d\n", poly_a[k]->intdim);
printf("realdim: %d\n", poly_a[k]->realdim);
printf("nbeq: %ld\n", poly_a[k]->nbeq);
printf("nbline: %ld\n", poly_a[k]->nbline);
printf("is_minimized: %d\n", poly_a[k]->is_minimized);
printf("status: %d\n", poly_a[k]->status);
printf("C->nbcolumns: %d\n", poly_a[k]->C->nbcolumns);
printf("C->nbrows: %ld\n", poly_a[k]->C->nbrows);
printf("F->nbcolumns: %d\n", poly_a[k]->F->nbcolumns);
printf("F->nbrows: %ld\n", poly_a[k]->F->nbrows);
printf("satC->nbcolumns: %ld\n", poly_a[k]->satC->nbcolumns);
printf("satC->nbrows: %ld\n", poly_a[k]->satC->nbrows);
if(!disjoint_map[k]){
printf("calling opt_poly_clear(poly_a[k])...\n");
opt_poly_clear(poly_a[k]);
printf("Call to opt_poly_clear(poly_a[k]) completed\n");
}
free(poly_a[k]);
}In addition, I've uncommented the 8 lines that follow this
https://github.com/eth-sri/ELINA/blob/9248e87b9ab2a425ed6fad6f71927aaddfd23f68/elina_poly/opt_pk_assign.c#L121
The end of the opt_poly_asssub_linexpr_det function looks like this:
op->poly = poly;
op->acl = acl;
free(exc_map);
printf("ASSIGN OUTPUT\n");
// print_array_comp_list(acl,op->maxcols);
elina_lincons0_array_t arr1 = opt_pk_to_lincons_array(man,op);
elina_lincons0_array_fprint(stdout, &arr1, NULL);
// elina_lincons0_array_clear(&arr1);
fflush(stdout);
printf("Exiting from opt_poly_asssub_linexpr_det");
return op;I can't uncomment this two functions (print_array_comp_list(acl,op->maxcols) and elina_lincons0_array_clear(&arr1)) because it crashes if I do it.
With this code, I get this results:
ASSIGN INPUT
0
empty array of constraints
x0:= 2147483648
ASSIGN OUTPUT
1
array of constraints of size 1
0: -x0 + 2147483648 = 0
Exiting from opt_poly_asssub_linexpr_det
ASSIGN INPUT
1
array of constraints of size 1
0: -x0 + 2147483648 = 0
x1:= x0
1
c
3
poly_a[k] data for k=0, num_compa=1:
intdim: 1
realdim: 0
nbeq: 1
nbline: 0
is_minimized: 0
status: 0
C->nbcolumns: 3
C->nbrows: 1
F->nbcolumns: 3
F->nbrows: 1
satC->nbcolumns: 1
satC->nbrows: 1
calling opt_poly_clear(poly_a[k])...
free(): invalid next size (fast)In the following days, I will take a look at my code and I will notify you to close the issues or to give you more details about the bug.
Thank you, Marius.
GgnDpSngh
commented
3 years ago Hi Marius,
Based on your trace, I created a sample program below which produces the same trace but did not observe any crash:
void test_assign(unsigned short int dim, size_t nbcons){ elina_manager_t man = opt_pk_manager_alloc(false); opt_pk_array_t oa1 = opt_pk_top(man, 2,0); //generate random constraints
elina_dim_t * tdim = (elina_dim_t *)malloc(sizeof(elina_dim_t));
tdim[0] = 0;
elina_linexpr0_t ** expr_array = (elina_linexpr0_t**)malloc(sizeof(elina_linexpr0_t*));
//elina_linexpr0_t * linexpr0 = generate_random_linexpr0(dim);
elina_coeff_t *cst, *coeff;
elina_linexpr0_t * linexpr0 = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE,0);
cst = &linexpr0->cst;
elina_scalar_set_to_int(cst->val.scalar,2147483648,ELINA_SCALAR_MPQ);
expr_array[0] = linexpr0;
printf("ELINA Input Polyhedron\n");
elina_lincons0_array_t arr1 = opt_pk_to_lincons_array(man,oa1);
elina_lincons0_array_fprint(stdout,&arr1,NULL);
printf("Assignment statement\n");
printf("x%d = ",tdim[0]);
elina_linexpr0_fprint(stdout,linexpr0,NULL);
printf("\n");
fflush(stdout);
elina_lincons0_array_clear(&arr1);
//assign;
opt_pk_assign_linexpr_array(man,true,oa1,tdim, expr_array,1,NULL);
elina_linexpr0_free(linexpr0);
// Print the result
printf("ELINA Output Polyhedron\n");
elina_lincons0_array_t arr = opt_pk_to_lincons_array(man,oa1);
elina_lincons0_array_fprint(stdout,&arr,NULL);
printf("\n");
fflush(stdout);
elina_lincons0_array_clear(&arr);
tdim[0] = 1;
linexpr0 = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE,1);
cst = &linexpr0->cst;
//int r = rand()%10;
elina_scalar_set_to_int(cst->val.scalar,0,ELINA_SCALAR_MPQ);
elina_linterm_t * linterm = &linexpr0->p.linterm[0];
linterm->dim = 0;
coeff = &linterm->coeff;
elina_scalar_set_to_int(coeff->val.scalar,1,ELINA_SCALAR_MPQ);
expr_array[0] = linexpr0;
//opt_pk_array_t * oa3 =
opt_pk_assign_linexpr_array(man,true,oa1,tdim, expr_array,1,NULL);
printf("ELINA Output Polyhedron\n");
arr = opt_pk_to_lincons_array(man,oa1);
elina_lincons0_array_fprint(stdout,&arr,NULL);
printf("\n");
fflush(stdout);
elina_lincons0_array_clear(&arr);
free(expr_array);
free(tdim);
opt_pk_free(man,oa1);
elina_manager_free(man);}
Make sure that you create polyhedra with >=2 variables as I did when calling the top function. Let me know if it helps.
Cheers, Gagandeep Singh
I've found a memory leak with Valgrind on the opt_poly manager. To be precise, in one of these functions (
opt_pk_assign_linexpr_array,opt_poly_asssub_linexproropt_poly_asssub_linexpr_det) of theopt_pk_assign.cfile.Below lists the Valgrind output:
Sorry for not providing a test case. You can ignore the functions
initStack,assignExpr*andelina_abstract1*. There are wrappers to ELINA (they are similar to the apron level 1 interface).In brief, I allocate a linexpr0 (
elina_linexpr0_alloc()), and then I assign an expression to it (elina_abstract0_asssub_linexpr_array).Thank you in advance!!