Skip to content

Commit 6cb0ef0

Browse files
AlexanderPortlandfeliperodri
AlexanderPortland
and
feliperodri
authored
Combo of small performance changes (#4314)
This PR is a pair of small performance changes. It used to be 4 (and thus would've been a real combo), but two involved caching so I've moved them under #4313 instead. These changes include: 1. passing information commonly used by our `GotocHook`s' `hook_applies` method as arguments, so that each hook doesn't have to recompute it on it's own 2. a small one-line change to compute a fn instance's name once instead of twice. These are both very small, but together with the other two changes now moved to #4313, made a ~6% decrease in the compile time of the standard library. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro <[email protected]>
1 parent c0c9ef8 commit 6cb0ef0

File tree

3 files changed

+183
-49
lines changed

3 files changed

+183
-49
lines changed

‎kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -728,8 +728,9 @@ impl GotocCtx<'_, '_> {
728728
let mut fargs = if args.is_empty()
729729
|| fn_def.fn_sig().unwrap().value.abi != Abi::RustCall
730730
{
731-
if instance.def.name() == "kani::internal::kani_forall"
732-
|| (instance.def.name() == "kani::internal::kani_exists")
731+
let fn_def_name = instance.def.name();
732+
if fn_def_name == "kani::internal::kani_forall"
733+
|| (fn_def_name == "kani::internal::kani_exists")
733734
{
734735
self.codegen_funcall_args_for_quantifiers(&fn_abi, args)
735736
} else {

‎kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs‎

Lines changed: 165 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111
use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label};
1212
use crate::codegen_cprover_gotoc::{GotocCtx, utils};
1313
use crate::kani_middle::attributes;
14-
use crate::kani_middle::kani_functions::{KaniFunction, KaniHook};
14+
use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, try_get_kani_function};
1515
use crate::unwrap_or_return_codegen_unimplemented_stmt;
1616
use cbmc::goto_program::CIntType;
1717
use cbmc::goto_program::Symbol as GotoSymbol;
@@ -30,7 +30,13 @@ use tracing::debug;
3030

3131
pub trait GotocHook {
3232
/// if the hook applies, it means the codegen would do something special to it
33-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool;
33+
fn hook_applies(
34+
&self,
35+
_tcx: TyCtxt,
36+
_instance: Instance,
37+
_instance_name: &str,
38+
_kani_tool_attr: Option<&String>,
39+
) -> bool;
3440
/// the handler for codegen
3541
fn handle(
3642
&self,
@@ -56,7 +62,13 @@ struct Cover;
5662
const UNEXPECTED_CALL: &str = "Hooks from kani library handled as a map";
5763

5864
impl GotocHook for Cover {
59-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
65+
fn hook_applies(
66+
&self,
67+
_tcx: TyCtxt,
68+
_instance: Instance,
69+
_instance_name: &str,
70+
_kani_tool_attr: Option<&String>,
71+
) -> bool {
6072
unreachable!("{UNEXPECTED_CALL}")
6173
}
6274

@@ -91,7 +103,13 @@ impl GotocHook for Cover {
91103

92104
struct Assume;
93105
impl GotocHook for Assume {
94-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
106+
fn hook_applies(
107+
&self,
108+
_tcx: TyCtxt,
109+
_instance: Instance,
110+
_instance_name: &str,
111+
_kani_tool_attr: Option<&String>,
112+
) -> bool {
95113
unreachable!("{UNEXPECTED_CALL}")
96114
}
97115

@@ -115,7 +133,13 @@ impl GotocHook for Assume {
115133

116134
struct Assert;
117135
impl GotocHook for Assert {
118-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
136+
fn hook_applies(
137+
&self,
138+
_tcx: TyCtxt,
139+
_instance: Instance,
140+
_instance_name: &str,
141+
_kani_tool_attr: Option<&String>,
142+
) -> bool {
119143
unreachable!("{UNEXPECTED_CALL}")
120144
}
121145

@@ -150,7 +174,13 @@ impl GotocHook for Assert {
150174

151175
struct UnsupportedCheck;
152176
impl GotocHook for UnsupportedCheck {
153-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
177+
fn hook_applies(
178+
&self,
179+
_tcx: TyCtxt,
180+
_instance: Instance,
181+
_instance_name: &str,
182+
_kani_tool_attr: Option<&String>,
183+
) -> bool {
154184
unreachable!("{UNEXPECTED_CALL}")
155185
}
156186

@@ -187,7 +217,13 @@ impl GotocHook for UnsupportedCheck {
187217

188218
struct SafetyCheck;
189219
impl GotocHook for SafetyCheck {
190-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
220+
fn hook_applies(
221+
&self,
222+
_tcx: TyCtxt,
223+
_instance: Instance,
224+
_instance_name: &str,
225+
_kani_tool_attr: Option<&String>,
226+
) -> bool {
191227
unreachable!("{UNEXPECTED_CALL}")
192228
}
193229

@@ -218,7 +254,13 @@ impl GotocHook for SafetyCheck {
218254

219255
struct SafetyCheckNoAssume;
220256
impl GotocHook for SafetyCheckNoAssume {
221-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
257+
fn hook_applies(
258+
&self,
259+
_tcx: TyCtxt,
260+
_instance: Instance,
261+
_instance_name: &str,
262+
_kani_tool_attr: Option<&String>,
263+
) -> bool {
222264
unreachable!("{UNEXPECTED_CALL}")
223265
}
224266

@@ -250,7 +292,13 @@ impl GotocHook for SafetyCheckNoAssume {
250292
// TODO: Remove this and replace occurrences with `SanityCheck`.
251293
struct Check;
252294
impl GotocHook for Check {
253-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
295+
fn hook_applies(
296+
&self,
297+
_tcx: TyCtxt,
298+
_instance: Instance,
299+
_instance_name: &str,
300+
_kani_tool_attr: Option<&String>,
301+
) -> bool {
254302
unreachable!("{UNEXPECTED_CALL}")
255303
}
256304

@@ -286,7 +334,13 @@ impl GotocHook for Check {
286334
struct Nondet;
287335

288336
impl GotocHook for Nondet {
289-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
337+
fn hook_applies(
338+
&self,
339+
_tcx: TyCtxt,
340+
_instance: Instance,
341+
_instance_name: &str,
342+
_kani_tool_attr: Option<&String>,
343+
) -> bool {
290344
unreachable!("{UNEXPECTED_CALL}")
291345
}
292346

@@ -325,9 +379,14 @@ impl GotocHook for Nondet {
325379
struct Panic;
326380

327381
impl GotocHook for Panic {
328-
fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
382+
fn hook_applies(
383+
&self,
384+
tcx: TyCtxt,
385+
instance: Instance,
386+
_instance_name: &str,
387+
kani_tool_attr: Option<&String>,
388+
) -> bool {
329389
let def_id = rustc_internal::internal(tcx, instance.def.def_id());
330-
let kani_tool_attr = attributes::fn_marker(instance.def);
331390

332391
// we check the attributes to make sure this hook applies to
333392
// panic functions we've stubbed too
@@ -354,7 +413,13 @@ impl GotocHook for Panic {
354413
/// Encodes __CPROVER_r_ok(ptr, size)
355414
struct IsAllocated;
356415
impl GotocHook for IsAllocated {
357-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
416+
fn hook_applies(
417+
&self,
418+
_tcx: TyCtxt,
419+
_instance: Instance,
420+
_instance_name: &str,
421+
_kani_tool_attr: Option<&String>,
422+
) -> bool {
358423
unreachable!("{UNEXPECTED_CALL}")
359424
}
360425

@@ -393,7 +458,13 @@ impl GotocHook for IsAllocated {
393458
/// independent of the backend
394459
struct FloatToIntInRange;
395460
impl GotocHook for FloatToIntInRange {
396-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
461+
fn hook_applies(
462+
&self,
463+
_tcx: TyCtxt,
464+
_instance: Instance,
465+
_instance_name: &str,
466+
_kani_tool_attr: Option<&String>,
467+
) -> bool {
397468
unreachable!("{UNEXPECTED_CALL}")
398469
}
399470

@@ -438,7 +509,13 @@ impl GotocHook for FloatToIntInRange {
438509
/// Encodes __CPROVER_pointer_object(ptr)
439510
struct PointerObject;
440511
impl GotocHook for PointerObject {
441-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
512+
fn hook_applies(
513+
&self,
514+
_tcx: TyCtxt,
515+
_instance: Instance,
516+
_instance_name: &str,
517+
_kani_tool_attr: Option<&String>,
518+
) -> bool {
442519
unreachable!("{UNEXPECTED_CALL}")
443520
}
444521

@@ -474,7 +551,13 @@ impl GotocHook for PointerObject {
474551
/// Encodes __CPROVER_pointer_offset(ptr)
475552
struct PointerOffset;
476553
impl GotocHook for PointerOffset {
477-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
554+
fn hook_applies(
555+
&self,
556+
_tcx: TyCtxt,
557+
_instance: Instance,
558+
_instance_name: &str,
559+
_kani_tool_attr: Option<&String>,
560+
) -> bool {
478561
unreachable!("{UNEXPECTED_CALL}")
479562
}
480563

@@ -511,9 +594,14 @@ struct RustAlloc;
511594
// Removing this hook causes regression failures.
512595
// https://github.com/model-checking/kani/issues/1170
513596
impl GotocHook for RustAlloc {
514-
fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool {
515-
let full_name = instance.name();
516-
full_name == "alloc::alloc::exchange_malloc"
597+
fn hook_applies(
598+
&self,
599+
_tcx: TyCtxt,
600+
_instance: Instance,
601+
instance_name: &str,
602+
_kani_tool_attr: Option<&String>,
603+
) -> bool {
604+
instance_name == "alloc::alloc::exchange_malloc"
517605
}
518606

519607
fn handle(
@@ -562,9 +650,14 @@ impl GotocHook for RustAlloc {
562650
pub struct MemCmp;
563651

564652
impl GotocHook for MemCmp {
565-
fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool {
566-
let name = instance.name();
567-
name == "core::slice::cmp::memcmp" || name == "std::slice::cmp::memcmp"
653+
fn hook_applies(
654+
&self,
655+
_tcx: TyCtxt,
656+
_instance: Instance,
657+
instance_name: &str,
658+
_kani_tool_attr: Option<&String>,
659+
) -> bool {
660+
instance_name == "core::slice::cmp::memcmp" || instance_name == "std::slice::cmp::memcmp"
568661
}
569662

570663
fn handle(
@@ -620,7 +713,13 @@ impl GotocHook for MemCmp {
620713
struct UntrackedDeref;
621714

622715
impl GotocHook for UntrackedDeref {
623-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
716+
fn hook_applies(
717+
&self,
718+
_tcx: TyCtxt,
719+
_instance: Instance,
720+
_instance_name: &str,
721+
_kani_tool_attr: Option<&String>,
722+
) -> bool {
624723
unreachable!("{UNEXPECTED_CALL}")
625724
}
626725

@@ -668,7 +767,13 @@ struct InitContracts;
668767
/// free(NULL);
669768
/// ```
670769
impl GotocHook for InitContracts {
671-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
770+
fn hook_applies(
771+
&self,
772+
_tcx: TyCtxt,
773+
_instance: Instance,
774+
_instance_name: &str,
775+
_kani_tool_attr: Option<&String>,
776+
) -> bool {
672777
unreachable!("{UNEXPECTED_CALL}")
673778
}
674779

@@ -710,9 +815,14 @@ impl GotocHook for InitContracts {
710815
pub struct LoopInvariantRegister;
711816

712817
impl GotocHook for LoopInvariantRegister {
713-
fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool {
714-
attributes::fn_marker(instance.def)
715-
.is_some_and(|marker| marker == "kani_register_loop_contract")
818+
fn hook_applies(
819+
&self,
820+
_tcx: TyCtxt,
821+
_instance: Instance,
822+
_instance_name: &str,
823+
kani_tool_attr: Option<&String>,
824+
) -> bool {
825+
kani_tool_attr.is_some_and(|marker| marker == "kani_register_loop_contract")
716826
}
717827

718828
fn handle(
@@ -785,7 +895,13 @@ enum QuantifierKind {
785895
}
786896

787897
impl GotocHook for Forall {
788-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
898+
fn hook_applies(
899+
&self,
900+
_tcx: TyCtxt,
901+
_instance: Instance,
902+
_instance_name: &str,
903+
_kani_tool_attr: Option<&String>,
904+
) -> bool {
789905
unreachable!("{UNEXPECTED_CALL}")
790906
}
791907

@@ -803,7 +919,13 @@ impl GotocHook for Forall {
803919
}
804920

805921
impl GotocHook for Exists {
806-
fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
922+
fn hook_applies(
923+
&self,
924+
_tcx: TyCtxt,
925+
_instance: Instance,
926+
_instance_name: &str,
927+
_kani_tool_attr: Option<&String>,
928+
) -> bool {
807929
unreachable!("{UNEXPECTED_CALL}")
808930
}
809931

@@ -951,15 +1073,21 @@ pub struct GotocHooks {
9511073

9521074
impl GotocHooks {
9531075
pub fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> Option<Rc<dyn GotocHook>> {
954-
if let Ok(KaniFunction::Hook(hook)) = KaniFunction::try_from(instance) {
955-
Some(self.kani_lib_hooks[&hook].clone())
956-
} else {
957-
for h in &self.other_hooks {
958-
if h.hook_applies(tcx, instance) {
959-
return Some(h.clone());
960-
}
1076+
let fn_attr = attributes::fn_marker(instance.def);
1077+
if let Some(ref fn_attr) = fn_attr
1078+
&& let Some(KaniFunction::Hook(hook)) = try_get_kani_function(fn_attr)
1079+
{
1080+
return Some(self.kani_lib_hooks[&hook].clone());
1081+
}
1082+
1083+
let instance_name = instance.name();
1084+
let kani_tool_attr = fn_attr.as_ref();
1085+
1086+
for h in &self.other_hooks {
1087+
if h.hook_applies(tcx, instance, &instance_name, kani_tool_attr) {
1088+
return Some(h.clone());
9611089
}
962-
None
9631090
}
1091+
None
9641092
}
9651093
}

0 commit comments

Comments
 (0)