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

Re-enabled hierarchical logs in the compiler #3449

Merged
merged 1 commit into from
Aug 22, 2024

Conversation

celinval
Copy link
Contributor

We reverted the hierarchical logs a while ago (#2581) due to an outdated dependency that has since been fixed.

I think this makes the logs much more readable, by indenting the logs given the scope. More than one scope makes the lines way too long, which I think it's harder to read.

This is how the logs look without this change:

2024-08-17T02:42:21.874979Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: handling kani::assert
2024-08-17T02:42:21.875008Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: variables:
2024-08-17T02:42:21.875026Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: let _0: Ty { id: 4, kind: RigidTy(Tuple([])) }

This is how it looks after this change:

┐kani_compiler::codegen_cprover_gotoc::codegen::function::CodegenFunction name="kani::assert"
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug handling kani::assert
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug variables:
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _0: Ty { id: 4, kind: RigidTy(Tuple([])) }
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _1: Ty { id: 6, kind: RigidTy(Bool) }

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

We reverted the hierarchical logs a while ago (model-checking#2581) due to an outdated
depedency that has since been fixed.

I think this makes the logs much more readable, by identing the logs
given the scope. More than one scope makes the lines way too long, which
I think it's harder to read.

This is how the logs look without this change:

```
2024-08-17T02:42:21.874979Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: handling kani::assert
2024-08-17T02:42:21.875008Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: variables:
2024-08-17T02:42:21.875026Z DEBUG CodegenFunction{name="kani::assert"}: kani_compiler::codegen_cprover_gotoc::utils::debug: let _0: Ty { id: 4, kind: RigidTy(Tuple([])) }

```

This is how it looks after this change:

```
┐kani_compiler::codegen_cprover_gotoc::codegen::function::CodegenFunction name="kani::assert"
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug handling kani::assert
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug variables:
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _0: Ty { id: 4, kind: RigidTy(Tuple([])) }
├─── DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _1: Ty { id: 6, kind: RigidTy(Bool) }

```
@celinval celinval requested a review from a team as a code owner August 17, 2024 02:49
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Aug 17, 2024
Copy link
Contributor

@jaisnan jaisnan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ty!

@celinval celinval added this pull request to the merge queue Aug 22, 2024
Merged via the queue into model-checking:main with commit 56e2a2f Aug 22, 2024
27 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Sep 4, 2024
These are the auto-generated release notes:

## What's Changed
* Update CBMC build instructions for Amazon Linux 2 by @tautschnig in
#3431
* Handle intrinsics systematically by @artemagvanian in
#3422
* Bump tests/perf/s2n-quic from `445f73b` to `ab9723a` by @dependabot in
#3434
* Automatic cargo update to 2024-08-12 by @github-actions in
#3433
* Actually apply CBMC patch by @tautschnig in
#3436
* Update features/verify-rust-std branch by @feliperodri in
#3435
* Add test related to issue 3432 by @celinval in
#3439
* Implement memory initialization state copy functionality by
@artemagvanian in #3350
* Bump tests/perf/s2n-quic from `ab9723a` to `80b93a7` by @dependabot in
#3453
* Make points-to analysis handle all intrinsics explicitly by
@artemagvanian in #3452
* Automatic cargo update to 2024-08-19 by @github-actions in
#3450
* Add loop scanner to tool-scanner by @qinheping in
#3443
* Avoid corner-cases by grouping instrumentation into basic blocks and
using backward iteration by @artemagvanian in
#3438
* Re-enabled hierarchical logs in the compiler by @celinval in
#3449
* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to
`str` by @celinval in #3448
* Automatic cargo update to 2024-08-26 by @github-actions in
#3459
* Bump tests/perf/s2n-quic from `80b93a7` to `8f7c04b` by @dependabot in
#3460
* Update deny action by @zhassan-aws in
#3461
* Basic support for memory initialization checks for unions by
@artemagvanian in #3444
* Adjust test patterns so as not to check for trivial properties by
@tautschnig in #3464
* Clarify comment in RFC Template by @carolynzech in
#3462
* RFC: Source-based code coverage by @adpaco-aws in
#3143
* Adopt Rust's source-based code coverage instrumentation by @adpaco-aws
in #3119
* Upgrade toolchain to 08/28 by @jaisnan in
#3454
* Extra tests and bug fixes to the delayed UB instrumentation by
@artemagvanian in #3419
* Upgrade Toolchain to 8/29 by @carolynzech in
#3468
* Automatic toolchain upgrade to nightly-2024-08-30 by @github-actions
in #3469
* Extend name resolution to support qualified paths (Partial Fix) by
@celinval in #3457
* Partially integrate uninit memory checks into `verify_std` by
@artemagvanian in #3470
* Update Toolchain to 9/1 by @carolynzech in
#3478
* Automatic cargo update to 2024-09-02 by @github-actions in
#3480
* Bump tests/perf/s2n-quic from `8f7c04b` to `1ff3a9c` by @dependabot in
#3481
* Automatic toolchain upgrade to nightly-2024-09-02 by @github-actions
in #3479
* Automatic toolchain upgrade to nightly-2024-09-03 by @github-actions
in #3482
* RFC for List Subcommand by @carolynzech in
#3463
* Add tests for fixed issues. by @carolynzech in
#3484


**Full Changelog**:
kani-0.54.0...kani-0.55.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants