Ruby: use overlayChangedFiles extensional in discard predicates

This commit is contained in:
Nick Rolfe
2025-06-27 12:19:52 +01:00
parent ba01a70e0a
commit d8574a6919
4 changed files with 33 additions and 67 deletions

View File

@@ -60,10 +60,6 @@ module QL {
)
}
/** Holds if `file` was extracted as part of the overlay database. */
overlay[local]
private predicate discardFile(@file file) { isOverlay() and file = getNodeFile(_) }
/** Holds if `node` is in the `file` and is part of the overlay base database. */
overlay[local]
private predicate discardableAstNode(@file file, @ql_ast_node node) {
@@ -73,7 +69,9 @@ module QL {
/** Holds if `node` should be discarded, because it is part of the overlay base and is in a file that was also extracted as part of the overlay database. */
overlay[discard_entity]
private predicate discardAstNode(@ql_ast_node node) {
exists(@file file | discardableAstNode(file, node) and discardFile(file))
exists(@file file, string path | files(file, path) |
discardableAstNode(file, node) and overlayChangedFiles(path)
)
}
/** A class representing `add_expr` nodes. */
@@ -1354,10 +1352,6 @@ module Dbscheme {
)
}
/** Holds if `file` was extracted as part of the overlay database. */
overlay[local]
private predicate discardFile(@file file) { isOverlay() and file = getNodeFile(_) }
/** Holds if `node` is in the `file` and is part of the overlay base database. */
overlay[local]
private predicate discardableAstNode(@file file, @dbscheme_ast_node node) {
@@ -1367,7 +1361,9 @@ module Dbscheme {
/** Holds if `node` should be discarded, because it is part of the overlay base and is in a file that was also extracted as part of the overlay database. */
overlay[discard_entity]
private predicate discardAstNode(@dbscheme_ast_node node) {
exists(@file file | discardableAstNode(file, node) and discardFile(file))
exists(@file file, string path | files(file, path) |
discardableAstNode(file, node) and overlayChangedFiles(path)
)
}
/** A class representing `annotName` tokens. */
@@ -1714,10 +1710,6 @@ module Blame {
)
}
/** Holds if `file` was extracted as part of the overlay database. */
overlay[local]
private predicate discardFile(@file file) { isOverlay() and file = getNodeFile(_) }
/** Holds if `node` is in the `file` and is part of the overlay base database. */
overlay[local]
private predicate discardableAstNode(@file file, @blame_ast_node node) {
@@ -1727,7 +1719,9 @@ module Blame {
/** Holds if `node` should be discarded, because it is part of the overlay base and is in a file that was also extracted as part of the overlay database. */
overlay[discard_entity]
private predicate discardAstNode(@blame_ast_node node) {
exists(@file file | discardableAstNode(file, node) and discardFile(file))
exists(@file file, string path | files(file, path) |
discardableAstNode(file, node) and overlayChangedFiles(path)
)
}
/** A class representing `blame_entry` nodes. */
@@ -1851,10 +1845,6 @@ module JSON {
)
}
/** Holds if `file` was extracted as part of the overlay database. */
overlay[local]
private predicate discardFile(@file file) { isOverlay() and file = getNodeFile(_) }
/** Holds if `node` is in the `file` and is part of the overlay base database. */
overlay[local]
private predicate discardableAstNode(@file file, @json_ast_node node) {
@@ -1864,7 +1854,9 @@ module JSON {
/** Holds if `node` should be discarded, because it is part of the overlay base and is in a file that was also extracted as part of the overlay database. */
overlay[discard_entity]
private predicate discardAstNode(@json_ast_node node) {
exists(@file file | discardableAstNode(file, node) and discardFile(file))
exists(@file file, string path | files(file, path) |
discardableAstNode(file, node) and overlayChangedFiles(path)
)
}
class UnderscoreValue extends @json_underscore_value, AstNode { }

View File

@@ -60,10 +60,6 @@ module Ruby {
)
}
/** Holds if `file` was extracted as part of the overlay database. */
overlay[local]
private predicate discardFile(@file file) { isOverlay() and file = getNodeFile(_) }
/** Holds if `node` is in the `file` and is part of the overlay base database. */
overlay[local]
private predicate discardableAstNode(@file file, @ruby_ast_node node) {
@@ -73,7 +69,9 @@ module Ruby {
/** Holds if `node` should be discarded, because it is part of the overlay base and is in a file that was also extracted as part of the overlay database. */
overlay[discard_entity]
private predicate discardAstNode(@ruby_ast_node node) {
exists(@file file | discardableAstNode(file, node) and discardFile(file))
exists(@file file, string path | files(file, path) |
discardableAstNode(file, node) and overlayChangedFiles(path)
)
}
class UnderscoreArg extends @ruby_underscore_arg, AstNode { }
@@ -2006,10 +2004,6 @@ module Erb {
)
}
/** Holds if `file` was extracted as part of the overlay database. */
overlay[local]
private predicate discardFile(@file file) { isOverlay() and file = getNodeFile(_) }
/** Holds if `node` is in the `file` and is part of the overlay base database. */
overlay[local]
private predicate discardableAstNode(@file file, @erb_ast_node node) {
@@ -2019,7 +2013,9 @@ module Erb {
/** Holds if `node` should be discarded, because it is part of the overlay base and is in a file that was also extracted as part of the overlay database. */
overlay[discard_entity]
private predicate discardAstNode(@erb_ast_node node) {
exists(@file file | discardableAstNode(file, node) and discardFile(file))
exists(@file file, string path | files(file, path) |
discardableAstNode(file, node) and overlayChangedFiles(path)
)
}
/** A class representing `code` tokens. */

View File

@@ -104,9 +104,6 @@ pub fn generate(
body.push(ql::TopLevel::Predicate(
ql_gen::create_get_node_file_predicate(&ast_node_name, &node_location_table_name),
));
body.push(ql::TopLevel::Predicate(
ql_gen::create_discard_file_predicate(),
));
body.push(ql::TopLevel::Predicate(
ql_gen::create_discardable_ast_node_predicate(&ast_node_name),
));

View File

@@ -318,34 +318,6 @@ pub fn create_get_node_file_predicate<'a>(
}
}
pub fn create_discard_file_predicate<'a>() -> ql::Predicate<'a> {
ql::Predicate {
name: "discardFile",
qldoc: Some(String::from(
"Holds if `file` was extracted as part of the overlay database.",
)),
overridden: false,
is_private: true,
is_final: false,
overlay: Some(ql::OverlayAnnotation::Local),
return_type: None,
formal_parameters: vec![ql::FormalParameter {
name: "file",
param_type: ql::Type::At("file"),
}],
body: ql::Expression::And(vec![
ql::Expression::Pred("isOverlay", vec![]),
ql::Expression::Equals(
Box::new(ql::Expression::Var("file")),
Box::new(ql::Expression::Pred(
"getNodeFile",
vec![ql::Expression::Var("_")],
)),
),
]),
}
}
pub fn create_discardable_ast_node_predicate(ast_node_name: &str) -> ql::Predicate {
ql::Predicate {
name: "discardableAstNode",
@@ -398,17 +370,26 @@ pub fn create_discard_ast_node_predicate(ast_node_name: &str) -> ql::Predicate {
}],
body: ql::Expression::Aggregate {
name: "exists",
vars: vec![ql::FormalParameter {
name: "file",
param_type: ql::Type::At("file"),
}],
range: None,
vars: vec![
ql::FormalParameter {
name: "file",
param_type: ql::Type::At("file"),
},
ql::FormalParameter {
name: "path",
param_type: ql::Type::String,
},
],
range: Some(Box::new(ql::Expression::Pred(
"files",
vec![ql::Expression::Var("file"), ql::Expression::Var("path")],
))),
expr: Box::new(ql::Expression::And(vec![
ql::Expression::Pred(
"discardableAstNode",
vec![ql::Expression::Var("file"), ql::Expression::Var("node")],
),
ql::Expression::Pred("discardFile", vec![ql::Expression::Var("file")]),
ql::Expression::Pred("overlayChangedFiles", vec![ql::Expression::Var("path")]),
])),
second_expr: None,
},