Prove read-only effects through current source call graphs

This commit is contained in:
2026-10-22 15:55:44 +08:00
parent cd25f819f2
commit ae821aea2e
11 changed files with 614 additions and 58 deletions
+32 -27
View File
@@ -111,33 +111,9 @@ impl EndorCode {
/// Unknown calls and writes remain unknown, even when they could be safe for
/// a particular invocation. New opcodes require an explicit audit here.
pub fn is_statically_read_only(&self) -> bool {
self.instructions.iter().all(|decoded| {
matches!(
decoded.instruction.opcode,
Opcode::Nop
| Opcode::LoadConst
| Opcode::LoadFast
| Opcode::DeleteFast
| Opcode::LoadGlobal
| Opcode::PopTop
| Opcode::Copy
| Opcode::Swap
| Opcode::PushNull
| Opcode::ReturnValue
| Opcode::JumpForward
| Opcode::JumpBackward
| Opcode::PopJumpIfFalse
| Opcode::PopJumpIfTrue
| Opcode::ToBool
| Opcode::UnaryNot
| Opcode::CompareOp
| Opcode::LoadDeref
| Opcode::LoadClosure
| Opcode::LoadAttr
| Opcode::BuildMap
| Opcode::MakeFunction
)
})
self.instructions
.iter()
.all(|decoded| read_only_opcode(decoded.instruction.opcode))
}
pub fn with_location(
@@ -262,6 +238,35 @@ impl ObjectPayload for EndorCodeObject {
}
}
// Shared by the local proof and call-graph analysis. Unknown opcodes fail closed.
pub(crate) fn read_only_opcode(opcode: Opcode) -> bool {
matches!(
opcode,
Opcode::Nop
| Opcode::LoadConst
| Opcode::LoadFast
| Opcode::DeleteFast
| Opcode::LoadGlobal
| Opcode::PopTop
| Opcode::Copy
| Opcode::Swap
| Opcode::PushNull
| Opcode::ReturnValue
| Opcode::JumpForward
| Opcode::JumpBackward
| Opcode::PopJumpIfFalse
| Opcode::PopJumpIfTrue
| Opcode::ToBool
| Opcode::UnaryNot
| Opcode::CompareOp
| Opcode::LoadDeref
| Opcode::LoadClosure
| Opcode::LoadAttr
| Opcode::BuildMap
| Opcode::MakeFunction
)
}
fn validate_layout(layout: &CodeLayout) -> Result<(), VmError> {
for names in [
&layout.parameters,