Skip to content

Improve kani-compiler logs#1000

Merged
celinval merged 3 commits intomodel-checking:mainfrom
celinval:main
Mar 31, 2022
Merged

Improve kani-compiler logs#1000
celinval merged 3 commits intomodel-checking:mainfrom
celinval:main

Conversation

@celinval
Copy link
Contributor

@celinval celinval commented Mar 30, 2022

Description of changes:

  1. Add option to force colored output. Before this change color was only enabled if running in TTY.
    • This is useful for IDEs and potentially to be used in cargo-kani.
  2. Add a few info_span to make the logs more readable.
    • This will indent the log related to each statement, in every function.

Resolved issues:

None

Call-outs:

Here is an example on how the debug looks like after the new info_span are added:

DEBUG kani_compiler::codegen_cprover_gotoc::utils::names finding function name for instance: harness, debug: Instance { def: Item(WithOptConstParam { did: DefId(0:4 ~ fixme_lib[afdc]::harness), const_param_did: None }), substs: [] }, name: harness, symbol: harness, demangle: harness
DEBUG kani_compiler::codegen_cprover_gotoc::utils::names finding function name for instance: harness, debug: Instance { def: Item(WithOptConstParam { did: DefId(0:4 ~ fixme_lib[afdc]::harness), const_param_did: None }), substs: [] }, name: harness, symbol: harness, demangle: harness
┐kani_compiler::codegen_cprover_gotoc::codegen::function::Codegen Function name="harness"
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug handling harness, harness
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug variables: 
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _1: i32
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _2: (i32, bool)
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _3: ()
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _4: bool
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug let _5: i32
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug block bb0
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug _1 = const 0_i32
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug goto -> bb1
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug block bb1
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug _2 = CheckedAdd(_1, const 1_i32)
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug assert(!move (_2.1: bool), "attempt to compute `{} + {}`, which would overflow", _1, const 1_i32) -> bb2
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug block bb2
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug _1 = move (_2.0: i32)
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug _5 = _1
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug _4 = Lt(move _5, const 10_i32)
├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::utils::debug _3 = kani::assert(move _4, const "assertion failed: counter < 10") -> bb1
├─┐
├───┐kani_compiler::codegen_cprover_gotoc::codegen::statement::CodegenStatement statement=_1 = const 0_i32
│   ├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::codegen::statement handling statement _1 = const 0_i32
│   ├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::codegen::place codegen_place: _1
│   ├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::codegen::operand codegen_scalar
│   │   0x00000000
│   │   i32
│   │   Some(fixme_lib.rs:17:23: 17:24 (#0))
│   │   Int(I32)
│ ┌─┘
├─┘
├─┐
├───┐kani_compiler::codegen_cprover_gotoc::codegen::statement::CodegenTerminator statement=goto -> bb1
│   ├───0ms DEBUG kani_compiler::codegen_cprover_gotoc::codegen::statement handling terminator Terminator { source_info: SourceInfo { span: fixme_lib.rs:18:5: 21:6 (#0), scope: scope[1] }, kind: goto -> bb1 }
│ ┌─┘
├─┘

Testing:

  • How is this change tested?

  • Is this a refactor change?

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

@celinval
Improve kani-compiler logs
e25f427 
 1. Add option to force colored output.
    - This is useful for IDEs and potentially to be used in cargo-kani.
 2. Add a few info_span to make the logs more readable.
    - This will indent the log related to each statement, in every
    function.
@celinval celinval requested a review from a team as a code owner March 30, 2022 22:33
@danielsn
Copy link
Contributor

danielsn commented Mar 31, 2022

Congrats on #1000!

@celinval celinval merged commit c7dacf4 into model-checking:main Mar 31, 2022
tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022
@celinval @tedinski
Improve kani-compiler logs (model-checking#1000)
b801243 
* Improve kani-compiler logs

 1. Add option to force colored output.
    - This is useful for IDEs and potentially to be used in cargo-kani.
 2. Add a few info_span to make the logs more readable.
    - This will indent the log related to each statement, in every
    function.
tedinski pushed a commit that referenced this pull request Apr 27, 2022
@celinval @tedinski
Improve kani-compiler logs (#1000)
361dc6e 
* Improve kani-compiler logs

 1. Add option to force colored output.
    - This is useful for IDEs and potentially to be used in cargo-kani.
 2. Add a few info_span to make the logs more readable.
    - This will indent the log related to each statement, in every
    function.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@zhassan-aws zhassan-aws zhassan-aws approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@celinval @danielsn @zhassan-aws