IntDomain code optimizations #943

mrstanb · 2022-12-06T10:37:50Z

This PR tackles some code optimization attempts in the intDomain.ml file. Namely:

There are currently 3 get_bool accesses to configuration flags of Goblint which can be stored in variables and looked up instead of being evaluated every time
Those 3 config flags which are being read with get_bool are:
ana.int.interval_threshold_widening
ana.int.interval_narrow_by_meet
ana.int.def_exc_widen_by_join

What we currently do as a solution is to store all 3 get_bool calls to mutable ref variables and just dereference said variables and use them in place of the original config lookups.

Note:

All runs where done on bench/coreutils/ls_comb.c as input
All runs are with Goblint, compiled with the flambda -O3 flag

For ana.int.interval_threshold_widening, the results are as follows (with the flags: --enable ana.int.interval and --enable ana.int.interval_threshold_widening):

Original run without code changes took very long and I just stopped it around 15 minutes in
After modifying the code, the run took 11.858s of walltime
Note: when running make test, the two tests which include the same set of flags for Goblint (namely 03/24 and 58/17) failed. Hence, some semantics might be broken by this change. We decided to keep it for now anyways and ask why the tests are failing exactly

For ana.int.interval_narrow_by_meet, the results are as follows (with the flags: --enable ana.int.interval and --enable ana.int.interval_narrow_by_meet):

Original run without code changes seemed to take long and I stopped after about 1 minute of running
After modifying the code, the run took 11.908s of walltime
Note: there were no test cases which were failing here, since there were no tests for this combination of Goblint flags

For ana.int.def_exc_widen_by_join, the results are more or less the same with and without code changes (roughly 12 seconds and with the flags --enable ana.int.def_exc and --enable ana.int.def_exc_widen_by_join):

Hence, this change could be possibly discarded, since it doesn't bring anything
We decided to keep it anyways in order to remain consistent with the other two changes, described above
Also, there were a few regression tests which include the set of these two flags (--enable ana.int.def_exc and --enable ana.int.def_exc_widen_by_join) which ran successfully both before and after the code changes here
Furthermore, make test ran successfully here both prior to and after the code changes
Thus, semantics here were most likely not broken (at least from what we saw from the passing make test run)

We would like to discuss the stated changes of the PR and see if they're viable and make sense.

mrstanb · 2022-12-06T10:40:10Z

Here are the three instructions that we used to run Goblint for this PR so far:

./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.interval --enable ana.int.interval_threshold_widening

./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.interval --enable ana.int.interval_narrow_by_meet

./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.def_exc --enable ana.int.def_exc_widen_by_join

mrstanb · 2022-12-06T10:42:06Z

Note: We decided to go for the bench/coreutils/ls_comb.c program as our input for Goblint due to the fact that it took the longest time to run among all the programs under bench/coreutils. We thought it'd make most sense to use a small program, yet the one which takes some more considerable time, compared to the others which were taking more like only a few seconds (ranging from 1 to about 5 or 6 seconds)

jerhard

Thanks for looking into this! I left some remark explaining why the issue with the failing tests is occurring.

jerhard · 2022-12-06T11:58:27Z

src/cdomains/intDomain.ml


  let cast_to ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)

+  let interval_threshold_widening_ref = ref @@ get_bool "ana.int.interval_threshold_widening"


This is a bit tricky here: This reference is set when the IntervalFunctor is instantiated, which is right at the start of the program, when the configuration is not yet read. Since the passed configuration is not read yet, the value that is passed for this configuration option cannot be retrieved at that point in time. This also should explain the failing test case. The same holds true for the other references.

An option would be to change this constant into a function that takes unit, and reads the configuration option when the function is first called, and later retrieves this stored value. Another alternative would be make the evaluation of the value lazy.

Thanks for the tip, make test now passes all tests after adding lazy evaluation of the bool value.

lazy will misbehave in server mode, because the option will only be read once. Our ResettableLazy would work around that, but if we really want to optimize this all the way, mutable variables would have the least overhead. The only thing is, they have to be initialized from options in a function, which is called after the options have been handled and reloaded in the server mode.

Since there are multiple of these cached options, instead of a bunch of refs, it's more convenient to use a record with mutable fields, which also avoids the additional indirection of a ref.

We also tried to do it with function that takes unit as mentioned above and also make test passes all tests

lazy will misbehave in server mode, because the option will only be read once. Our ResettableLazy would work around that, but if we really want to optimize this all the way, mutable variables would have the least overhead. The only thing is, they have to be initialized from options in a function, which is called after the options have been handled and reloaded in the server mode.

Since there are multiple of these cached options, instead of a bunch of refs, it's more convenient to use a record with mutable fields, which also avoids the additional indirection of a ref.

Thanks for the feedback! We'll make sure to look into the solution with a record in place of a ref. Currently we have a solution with a ref variable which passes make test and has the best running time out of all attempts. Hence, we now have to optimize this with a record, as you suggested.

jerhard · 2022-12-06T12:08:56Z

After modifying the code, the run took 11.858s of walltime

This is probably because the option to use the threshold widening (which is expensive) is not picked up, see my comment above.

mrstanb · 2022-12-06T12:58:27Z

@jerhard Thanks a lot for the input and the feedback! We'll look into the options that you suggested :)

mrstanb · 2022-12-13T15:23:07Z

We refactored the mutable variable way of reading config options and moved it into its own module in the configUtil.ml file.
We also tried to replace all get_bool and get_string calls in analyses/base.ml, however this lead to a slower runtime, compared to when only optimizing in the cdomains/intDomain.ml file. We decided to keep the commit for reference for now, but we can get rid of it later.
make test runs through for this case as well

jerhard · 2022-12-20T12:50:02Z

src/analyses/base.ml

              ) st sets
          )
+        |> List.of_seq
        |> BatList.fold_left D.meet st


Could one just use the fold_left on Seq here?

Thanks for the tip, I tried it and it seems to work fine, so I will try to run Goblint now and see if we get any improvements.

Seq.map and Seq.fold_left are fine, but one has to be careful using Seq functions, because many were just added in OCaml 4.14, while we also support 4.10: https://v2.ocaml.org/api/Seq.html.

mrstanb · 2022-12-20T13:58:16Z

I changed the current config value reading optimization as follows:

Instead of having to perform a bunch of string matches in the config util functions (get_bool_config_value and get_string_config_value), I know added a type with multiple constructors which aim to replace the strings that were being matched in the guards of these two functions
I also split the one huge record with various config values into separate config value records, based on common config options
This was done in commit 696feb7
I went to run the following at this commit:

./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.interval --enable ana.int.interval_threshold_widening

and the running time was still not very impressive, namely 1430.971s of walltime.

Due to this result, we decided to try and slim down the config optimization code a bit and avoid the get_bool_config_value and get_string_config_value functions now altogether.

Please let us know in case you also have any remarks

mrstanb · 2022-12-20T15:39:51Z

I changed the current config value reading optimization as follows:

Instead of having to perform a bunch of string matches in the config util functions (get_bool_config_value and get_string_config_value), I know added a type with multiple constructors which aim to replace the strings that were being matched in the guards of these two functions

I also split the one huge record with various config values into separate config value records, based on common config options

This was done in commit 696feb7

I went to run the following at this commit:
./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.interval --enable ana.int.interval_threshold_widening
and the running time was still not very impressive, namely 1430.971s of walltime.

Due to this result, we decided to try and slim down the config optimization code a bit and avoid the get_bool_config_value and get_string_config_value functions now altogether.

Please let us know in case you also have any remarks

This brought us again in the ball-park of ~1456s of walltime

mrstanb · 2022-12-20T16:02:37Z

Also tried to put all the configUtil module things back to intDomain which brought a speed up to around 1317.498s

mrstanb · 2023-01-13T12:01:50Z

Regarding the difference between using refs and records for storing the already read config options, some benchmarks were done on my personal laptop, as well as on the cluster:

On my personal laptop the following benchmarks were observed:

With flambda:

No optimizations in intDomain (no ref and no record; commit 0534c15137): 1039.263s
With the ref optimization (commit e6a76810dc): 997.368s
With record in place of ref (commit 907247740d): 1060.920s

Without flambda:

No optimizations in intDomain (no ref and no record; commit 0534c15137): 1137.535s
With the ref optimization (commit e6a76810dc): 1398.477s
With record in place of ref (commit 907247740d): 1440.362s

On the cluster the following benchmarks were observed:

With flambda:

No optimizations in intDomain (no ref and no record; commit 0534c15137): 1184.228s
With the ref optimization (commit e6a76810dc): 1274.162s
With record in place of ref (commit 907247740d): 1239.015s

Without flambda:

No optimizations in intDomain (no ref and no record; commit 0534c15137): 1428.567s
With the ref optimization (commit e6a76810dc): 1397.596s
With record in place of ref (commit 907247740d): 1305.515s

mrstanb · 2023-01-13T12:08:58Z

According to my last comment (#943 (comment)), I'm not sure if changing the way that configs are read is really necessary, considering the fact that the speed-up is not so dramatic.
@jerhard @sim642 could you please also provide your feedback and opinions on this?

sim642 · 2023-01-16T09:08:42Z

Instead of having to perform a bunch of string matches in the config util functions (get_bool_config_value and get_string_config_value), I know added a type with multiple constructors which aim to replace the strings that were being matched in the guards of these two functions

I didn't have a look at the current state of this PR yet, but just an interesting tidbit: the compilation of matches over constant strings is highly efficient in OCaml: https://discuss.ocaml.org/t/constant-string-pattern-matching/10801.

sim642

This needs to be rebased onto the current master after #928.

src/cdomains/intDomain.ml

src/analyses/base.ml

src/cdomains/intDomain.ml

michael-schwarz · 2023-01-18T19:27:43Z

Please rebase this PR, it is currently very hard to review since it includes both changes due to flambda, Seq, and the actual optimization.

sim642

Was there no need to cache the int domain activation options like ana.int.interval? I recall from profiling a while ago that those also were noticeable.

README.md

src/cdomains/intDomain.ml

…ontextUtil

mrstanb · 2023-02-09T09:15:25Z

Was there no need to cache the int domain activation options like ana.int.interval? I recall from profiling a while ago that those also were noticeable.

I tried some further optimization for the activation options of the integer domains in the precisionUtil.ml file with some changes in the contextUtil.ml file. Commit d5ae8ea reflects these changes.

Below I'll post some runs that I did locally on my machine which show some speed-up for the `ls_comb.c` program as input:

4 runs without optimization (with ls_comb.c as input):

with ana.int.interval -> 15.283s
with ana.int.def_exc -> 15.214s
with ana.int.enums -> 15.370s
with ana.int.congruence -> 13.945s

4 runs with optimization (with ls_comb.c as input):

with ana.int.interval -> 14.466s
with ana.int.def_exc -> 14.488s
with ana.int.enums -> 14.386s
with ana.int.congruence -> 14.507s

4 runs without optimization (with ls_comb.c as input):

with ana.int.interval + annotation.int.enabled -> 19.078s
with ana.int.def_exc + annotation.int.enabled -> 19.136s
with ana.int.enums + annotation.int.enabled -> 18.822s
with ana.int.congruence + annotation.int.enabled -> 17.605s

4 runs with optimization (with ls_comb.c as input):

with ana.int.interval + annotation.int.enabled -> 16.523s
with ana.int.def_exc + annotation.int.enabled -> 16.447s
with ana.int.enums + annotation.int.enabled -> 16.225s
with ana.int.congruence + annotation.int.enabled -> 16.322s

Note 1: with optimization means with the changes from commit d5ae8ea
Note 2: both the with optimization and without optimization runs that I did were run without the changes, provided in commit 017a721, since I wasn't sure if this commit is correct and whether it preserves Goblint's soundness.

mrstanb · 2023-02-09T09:25:56Z

Note: make test fails from commit 7c2455a onward and it runs through successfully for commit 017a721.

Any ideas or insights as to what could be wrong with the optimization changes in commit 017a721?

sim642 · 2023-02-09T10:25:16Z

The PrecisionUtil options also need a way to reset them in server mode, although that's not directly the issue because the tests aren't in server mode.

I suspect somewhere something is done with the int domains before the config is read, so the default activations are cached and any options activating more int domains are ignored. Maybe some debug printing/exception raising in those functions which do the caching reveal when it happens.

This broke int domain activation caching in 7c2455a.

sim642 · 2023-02-16T10:07:08Z

The PrecisionUtil options also need a way to reset them in server mode, although that's not directly the issue because the tests aren't in server mode.

I fixed this by adding a corresponding reset_lazy function.

I suspect somewhere something is done with the int domains before the config is read, so the default activations are cached and any options activating more int domains are ignored. Maybe some debug printing/exception raising in those functions which do the caching reveal when it happens.

The problem was caused by FloatDomain eagerly constructing IntDomain elements during initialization (when config hasn't been handled yet). I fixed this by converting some values to unit functions.

sim642

This PR history contains some old flambda stuff and lots of back-and-forth, so a squash merge would be appropriate here.

michael-schwarz

LGTM, thanks everyone from the team, and thank you @sim642 for the improvements!

I'd suggest we wait with merging this until after ~~#966~~ #994 is landed. These two PRs conflict and given this one is a lot smaller, it'll be easier than the other way around.

mrstanb · 2023-02-25T08:10:44Z

I ran some further benchmarks on this branch, compared to the current latest state of the master branch to see if we have some speed-up from this branch's optimizations at the end of the day. Below you can find the results (input program was ls_comb.c):

On `master` branch (commit `22a720c`)

With `ana.int.def_exc` and `annotation.int.enabled`:

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.def_exc --enable annotation.int.enabled
Time: 13.589s

With `ana.int.interval` and `annotation.int.enabled`

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --disable ana.int.def_exc --enable ana.int.interval --enable annotation.int.enabled
Time: 14.251s

With `ana.int.enums` and `annotation.int.enabled`

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --disable ana.int.def_exc --enable ana.int.enums --enable annotation.int.enabled
Time: 13.809s

With `ana.int.congruence` and `annotation.int.enabled`

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --disable ana.int.def_exc --enable ana.int.congruence --enable annotation.int.enabled
Time: 13.369s

On `int-domain-code-optimizations` branch (commit `7fb540e`)

With `ana.int.def_exc` and `annotation.int.enabled`:

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --enable ana.int.def_exc --enable annotation.int.enabled
Time: 12.293s

With `ana.int.interval` and `annotation.int.enabled`:

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --disable ana.int.def_exc --enable ana.int.interval --enable annotation.int.enabled
Time: 12.102s

With `ana.int.enums` and `annotation.int.enabled`:

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --disable ana.int.def_exc --enable ana.int.enums --enable annotation.int.enabled
Time: 12.248s

With `ana.int.congruence` and `annotation.int.enabled`:

Command: ./goblint ../bench/coreutils/ls_comb.c --set pre.cppflags[+] "--std=gnu89" --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper --enable dbg.timing.enabled --disable ana.int.def_exc --enable ana.int.congruence --enable annotation.int.enabled
Time: 11.522s

sim642 added student-job performance Analysis time, memory usage pr-dependency Depends or builds on another PR, which should be merged before labels Dec 6, 2022

jerhard reviewed Dec 6, 2022

View reviewed changes

sim642 self-requested a review December 6, 2022 13:20

jerhard reviewed Dec 20, 2022

View reviewed changes

montrie mentioned this pull request Jan 9, 2023

Iter optimization #964

Closed

sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Jan 16, 2023

sim642 requested changes Jan 16, 2023

View reviewed changes

src/cdomains/intDomain.ml Outdated Show resolved Hide resolved

src/cdomains/intDomain.ml Outdated Show resolved Hide resolved

src/analyses/base.ml Outdated Show resolved Hide resolved

michael-schwarz reviewed Jan 18, 2023

View reviewed changes

src/cdomains/intDomain.ml Outdated Show resolved Hide resolved

michael-schwarz added the practical-course Practical Course at TUM label Jan 18, 2023

mrstanb and others added 7 commits January 19, 2023 11:04

Update make.sh to also install ocaml with flambda

a6a4972

Update make.sh for the right flambda switch + update goblint.opam.locked

f0ed9a2

Remove eval from opam_setup_flambda

9f8fbf2

Update README with flambda installation info

3be6067

added lazy evaluation

9b8a1dd

Replace frequent get_bool calls with variable lookups

4c11f90

Memoize config value for ana.int.interval_threshold_widening

0230f6b

mrstanb added 2 commits January 31, 2023 12:15

Bring base.ml back to how it was (and fix indentation errors there)

ca8945b

Fix indentation error in base.ml

d98d4b3

sim642 requested changes Feb 2, 2023

View reviewed changes

README.md Outdated Show resolved Hide resolved

src/cdomains/intDomain.ml Show resolved Hide resolved

mrstanb added 5 commits February 8, 2023 19:48

Remove README autoformatting changes

1bd3e9b

More README formatting fixes

a5f638d

Reset record values in intDomain when resetting lazy values

017a721

Optimize with ref variables for config reading in precisionUtil and c…

7c2455a

…ontextUtil

Fix indent issues

d5ae8ea

sim642 self-requested a review February 9, 2023 09:17

sim642 self-assigned this Feb 9, 2023

sim642 added 5 commits February 16, 2023 10:37

Fix FloatDomain accessing IntDomain options at initialization time

a491a8f

This broke int domain activation caching in 7c2455a.

Merge branch 'master' into int-domain-code-optimizations

b564581

Revert unrelated changes

812d627

Reset PrecisionUtil option caching in server mode

4f158fc

Fix FloatDomainTest by resetting cached int domain activations

7fb540e

sim642 approved these changes Feb 16, 2023

View reviewed changes

sim642 requested a review from michael-schwarz February 16, 2023 10:08

michael-schwarz approved these changes Feb 19, 2023

View reviewed changes

Merge branch 'master' into int-domain-code-optimizations

07a2af4

sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Feb 27, 2023

sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Mar 21, 2023

Merge branch 'master' into int-domain-code-optimizations

5ea4c87

sim642 merged commit 01f8365 into goblint:master Mar 21, 2023

sim642 added a commit that referenced this pull request Mar 21, 2023

Fix indentation (PR #943)

318f407

sim642 added this to the v2.2.0 milestone Apr 5, 2023


		let cast_to ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)

		let interval_threshold_widening_ref = ref @@ get_bool "ana.int.interval_threshold_widening"

IntDomain code optimizations #943

IntDomain code optimizations #943

Uh oh!

Conversation

mrstanb commented Dec 6, 2022

Uh oh!

mrstanb commented Dec 6, 2022

Uh oh!

mrstanb commented Dec 6, 2022

Uh oh!

jerhard left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jerhard commented Dec 6, 2022

Uh oh!

mrstanb commented Dec 6, 2022

Uh oh!

mrstanb commented Dec 13, 2022

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mrstanb commented Dec 20, 2022

Uh oh!

mrstanb commented Dec 20, 2022

Uh oh!

mrstanb commented Dec 20, 2022

Uh oh!

mrstanb commented Jan 13, 2023

On my personal laptop the following benchmarks were observed:

With flambda:

Without flambda:

On the cluster the following benchmarks were observed:

With flambda:

Without flambda:

Uh oh!

mrstanb commented Jan 13, 2023

Uh oh!

sim642 commented Jan 16, 2023

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

michael-schwarz commented Jan 18, 2023

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

mrstanb commented Feb 9, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Below I'll post some runs that I did locally on my machine which show some speed-up for the ls_comb.c program as input:

Uh oh!

mrstanb commented Feb 9, 2023

Uh oh!

sim642 commented Feb 9, 2023

Uh oh!

sim642 commented Feb 16, 2023

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

jerhard left a comment •

edited

Loading

mrstanb commented Feb 9, 2023 •

edited

Loading

Below I'll post some runs that I did locally on my machine which show some speed-up for the `ls_comb.c` program as input:

michael-schwarz left a comment •

edited

Loading

On `master` branch (commit `22a720c`)

With `ana.int.def_exc` and `annotation.int.enabled`:

With `ana.int.interval` and `annotation.int.enabled`

With `ana.int.enums` and `annotation.int.enabled`

With `ana.int.congruence` and `annotation.int.enabled`

On `int-domain-code-optimizations` branch (commit `7fb540e`)

With `ana.int.def_exc` and `annotation.int.enabled`:

With `ana.int.interval` and `annotation.int.enabled`:

With `ana.int.enums` and `annotation.int.enabled`:

With `ana.int.congruence` and `annotation.int.enabled`: