Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add malloc align test #118

Merged
merged 1 commit into from
Jan 26, 2024
Merged

Conversation

krtab
Copy link
Collaborator

@krtab krtab commented Jan 22, 2024

Add a test for malloc well-alignedness.

The test is pretty long to run (8 sec on my machine).

Depends on #104

@krtab krtab force-pushed the add_malloc_align_test branch from db7c557 to 8ab70f6 Compare January 22, 2024 13:11
@krtab
Copy link
Collaborator Author

krtab commented Jan 22, 2024

Actually, rewriting the test as below (adding assumes) bring the run time to ~3 secs.

@krtab krtab force-pushed the add_malloc_align_test branch from 8ab70f6 to 779c975 Compare January 22, 2024 13:13
@zapashcanon
Copy link
Member

Thanks! Do you want to try adding a dune rule yourself so that it becomes part of dune runtest or should I do it ?

@krtab
Copy link
Collaborator Author

krtab commented Jan 22, 2024

I'm not sure we should add it given its large run time.

@krtab krtab force-pushed the add_malloc_align_test branch from 779c975 to 530f6b9 Compare January 22, 2024 17:35
@filipeom
Copy link
Collaborator

Thanks for the test @krtab!! There's a bug regarding the Ptr type returned by owi_alloc. I just ran this locally, and with -w 8 owi is making 8200 calls to the solver, totaling 34s in the solver. This means that the expressions in owi_assert, i.e., stuff like this:

calling func : func owi_assert
stack        : [  ]
running instr: local.get 0
stack        : [ (i32.of_bool (i32.eq (i32.rem (Ptr (i32 8390672) (i32 0)) (i32 1)) (i32 0))) ]

Is being discharged to the solver instead of being solved concretely

@krtab
Copy link
Collaborator Author

krtab commented Jan 25, 2024

ee66c6a is actually in #127 which should be merged first

@krtab
Copy link
Collaborator Author

krtab commented Jan 25, 2024

Performance issue fixed in https://github.com/formalsec/encoding/pull/65

@krtab krtab force-pushed the add_malloc_align_test branch from c89c234 to ee70339 Compare January 25, 2024 22:49
@zapashcanon
Copy link
Member

Could you run dune fmt and commit the formatted dune file ? :-)

Otherwise, should I merge this ? It's all OK for me.

@krtab krtab force-pushed the add_malloc_align_test branch from ee70339 to 59ae4ed Compare January 26, 2024 15:01
@krtab
Copy link
Collaborator Author

krtab commented Jan 26, 2024

Otherwise, should I merge this ? It's all OK for me.

Yes, the slight performance issue will be fixed once we merge hashconsing in encoding so 🟢

@zapashcanon zapashcanon merged commit ad96c9a into OCamlPro:main Jan 26, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants