Skip to content

Commit c23fb6f

Browse files
theo25theo25
authored
No proof hint events for unit/elememt collection hooks (#1150)
The unit/element hooks for collections are not useful to the math proof team so we modify our instrumentation to not emit them at all.
1 parent 4c858f4 commit c23fb6f

File tree

104 files changed

+11
-4291
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

104 files changed

+11
-4291
lines changed

‎lib/codegen/CreateTerm.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -693,6 +693,12 @@ llvm::Value *create_term::create_hardcoded_hook(
693693
return nullptr;
694694
}
695695

696+
static bool hook_is_collection_unit_or_element(std::string const &name) {
697+
return name == "LIST.unit" || name == "LIST.element" || name == "MAP.unit"
698+
|| name == "MAP.element" || name == "SET.unit" || name == "SET.element"
699+
|| name == "RANGEMAP.unit" || name == "RANGEMAP.element";
700+
}
701+
696702
llvm::Value *create_term::create_hook(
697703
kore_composite_pattern *hook_att, kore_composite_pattern *pattern,
698704
std::string const &location_stack) {
@@ -715,6 +721,11 @@ llvm::Value *create_term::create_hook(
715721
enable_gc(old_val);
716722
}
717723

724+
if (hook_is_collection_unit_or_element(name)) {
725+
// no proof trace event generation for unit/element collection hooks
726+
return result;
727+
}
728+
718729
proof_event e(definition_, module_);
719730
current_block_
720731
= e.hook_event_pre(name, pattern, current_block_, location_stack);

‎test/output/add-rewrite/input.proof.debug.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,4 @@
11
version: 13
2-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
3-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
4-
arg: kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
5-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
6-
hook: MAP.unit Lbl'Stop'Map{} ()
7-
hook result: kore[Lbl'Stop'Map{}()]
82
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
93
arg: kore[Lbl'Stop'Map{}()]
104
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]

‎test/output/add-rewrite/input.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,4 @@
11
version: 13
2-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
3-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
4-
arg: kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
5-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
6-
hook: MAP.unit Lbl'Stop'Map{} ()
7-
hook result: kore[Lbl'Stop'Map{}()]
82
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
93
arg: kore[Lbl'Stop'Map{}()]
104
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]

‎test/output/arith/add.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,4 @@
11
version: 13
2-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
3-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
4-
arg: kore[Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2")))]
5-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))))]
6-
hook: MAP.unit Lbl'Stop'Map{} ()
7-
hook result: kore[Lbl'Stop'Map{}()]
82
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
93
arg: kore[Lbl'Stop'Map{}()]
104
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))))]

‎test/output/arith/well.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,4 @@
11
version: 13
2-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
3-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
4-
arg: kore[Lblwell'LParUndsCommUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp'Unds'Exp{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("5"),\dv{SortInt{}}("10")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("3"),\dv{SortInt{}}("4")))]
5-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblwell'LParUndsCommUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp'Unds'Exp{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("5"),\dv{SortInt{}}("10")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("3"),\dv{SortInt{}}("4"))))]
6-
hook: MAP.unit Lbl'Stop'Map{} ()
7-
hook result: kore[Lbl'Stop'Map{}()]
82
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
93
arg: kore[Lbl'Stop'Map{}()]
104
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblwell'LParUndsCommUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp'Unds'Exp{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("2"))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("5"),\dv{SortInt{}}("10")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(\dv{SortInt{}}("3"),\dv{SortInt{}}("4"))))]

‎test/output/assoc-function/left.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Und
1111
rule: 103 2
1212
Var'Unds'X = kore[Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
1313
VarY = kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
14-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
15-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
16-
arg: kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
17-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
18-
hook: MAP.unit Lbl'Stop'Map{} ()
19-
hook result: kore[Lbl'Stop'Map{}()]
2014
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
2115
arg: kore[Lbl'Stop'Map{}()]
2216
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]

‎test/output/assoc-function/next-left.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Und
1111
rule: 103 2
1212
Var'Unds'X = kore[Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
1313
VarY = kore[Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
14-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
15-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
16-
arg: kore[Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
17-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()))]
18-
hook: MAP.unit Lbl'Stop'Map{} ()
19-
hook result: kore[Lbl'Stop'Map{}()]
2014
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
2115
arg: kore[Lbl'Stop'Map{}()]
2216
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()))]

‎test/output/assoc-function/next-right.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Un
1111
rule: 104 2
1212
Var'Unds'Y = kore[Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
1313
VarX = kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
14-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
15-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
16-
arg: kore[Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
17-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()))]
18-
hook: MAP.unit Lbl'Stop'Map{} ()
19-
hook result: kore[Lbl'Stop'Map{}()]
2014
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
2115
arg: kore[Lbl'Stop'Map{}()]
2216
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()))]

‎test/output/assoc-function/right.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,6 @@ function: Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Un
1111
rule: 104 2
1212
Var'Unds'Y = kore[Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
1313
VarX = kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
14-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
15-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
16-
arg: kore[Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()]
17-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]
18-
hook: MAP.unit Lbl'Stop'Map{} ()
19-
hook result: kore[Lbl'Stop'Map{}()]
2014
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
2115
arg: kore[Lbl'Stop'Map{}()]
2216
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())]

‎test/output/builtin-functions/abs.proof.out.diff

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,12 +14,6 @@ hook: KEQUAL.ite Lblite{SortInt{}} ()
1414
arg: kore[\dv{SortBool{}}("true")]
1515
arg: kore[\dv{SortInt{}}("5")]
1616
hook result: kore[\dv{SortInt{}}("5")]
17-
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
18-
arg: kore[\dv{SortKConfigVar{}}("$PGM")]
19-
arg: kore[\dv{SortInt{}}("5")]
20-
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortInt{}}("5"))]
21-
hook: MAP.unit Lbl'Stop'Map{} ()
22-
hook result: kore[Lbl'Stop'Map{}()]
2317
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
2418
arg: kore[Lbl'Stop'Map{}()]
2519
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortInt{}}("5"))]

0 commit comments

Comments
 (0)