Skip to content

Commit 8d4cdb8

Browse files
authored
feat: Add pcode-op bound and tweak computed valuation (#212)
* Add pcode-op bound and SimpleValue addresses * Add Indirect variant to PcodeAddressLattice Return Indirect for BranchInd/CallInd/Return transfer results and store IndirectVarNode. Strengthen BasicLocationState from valuation.indirect_writes, resolving to Const or Computed when possible. Add formatting/Debug/LowerHex support and update ordering/join behavior. Minor cleanup in BoundedBranchState PartialOrd and imports. * Skip Top when strengthening and keep branch target * fmt + clippy
1 parent 0c12f95 commit 8d4cdb8

File tree

5 files changed

+116
-48
lines changed

5 files changed

+116
-48
lines changed

jingle/src/analysis/cpa/lattice/pcode.rs

Lines changed: 43 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
use crate::analysis::cpa::lattice::JoinSemiLattice;
22
use crate::analysis::cpa::state::{AbstractState, LocationState, MergeOutcome, Successor};
3+
use crate::analysis::valuation::SimpleValue;
34
use crate::display::JingleDisplay;
45
use crate::modeling::machine::cpu::concrete::ConcretePcodeAddress;
56
use jingle_sleigh::{IndirectVarNode, PcodeOperation};
@@ -13,12 +14,14 @@ use std::iter::{empty, once};
1314
///
1415
/// Variants:
1516
/// - `Const(addr)` — a concrete pcode address (like `FlatLattice::Value`)
16-
/// - `Computed(indirect)` — a location that may be computed from an indirect varnode
17+
/// - `Indirect(ivn)` — raw output of the transfer function for indirect branches
18+
/// - `Computed(sv)` — resolved by valuation strengthening
1719
/// - `Top` — unknown / multiple locations
1820
#[derive(Clone, PartialEq, Eq, Hash)]
1921
pub enum PcodeAddressLattice {
2022
Const(ConcretePcodeAddress),
21-
Computed(IndirectVarNode),
23+
Indirect(IndirectVarNode),
24+
Computed(SimpleValue),
2225
Top,
2326
}
2427

@@ -30,9 +33,8 @@ impl JingleDisplay for PcodeAddressLattice {
3033
) -> std::fmt::Result {
3134
match self {
3235
PcodeAddressLattice::Const(addr) => write!(f, "{:x}", addr),
33-
PcodeAddressLattice::Computed(indirect_var_node) => {
34-
indirect_var_node.fmt_jingle(f, info)
35-
}
36+
PcodeAddressLattice::Indirect(ivn) => ivn.fmt_jingle(f, info),
37+
PcodeAddressLattice::Computed(sv) => sv.fmt_jingle(f, info),
3638
PcodeAddressLattice::Top => write!(f, "Top"),
3739
}
3840
}
@@ -45,6 +47,10 @@ impl Debug for PcodeAddressLattice {
4547
.debug_tuple("PcodeAddressLattice::Const")
4648
.field(&format_args!("{:x}", a))
4749
.finish(),
50+
PcodeAddressLattice::Indirect(ivn) => f
51+
.debug_tuple("PcodeAddressLattice::Indirect")
52+
.field(&format_args!("{:?}", ivn))
53+
.finish(),
4854
PcodeAddressLattice::Computed(c) => f
4955
.debug_tuple("PcodeAddressLattice::Computed")
5056
.field(&format_args!("{:?}", c))
@@ -60,9 +66,11 @@ impl LowerHex for PcodeAddressLattice {
6066
// Delegate to the inner `ConcretePcodeAddress` LowerHex implementation
6167
// so `{:#x}` / `{:x}` on `PcodeAddressLattice::Const` prints the expected hex form.
6268
PcodeAddressLattice::Const(a) => write!(f, "PcodeAddressLattice::Const({:x})", a),
63-
// Computed values don't have a natural hex representation; fall back to debug.
64-
PcodeAddressLattice::Computed(c) => {
65-
write!(f, "PcodeAddressLattice::Computed({:?})", c)
69+
PcodeAddressLattice::Indirect(ivn) => {
70+
write!(f, "PcodeAddressLattice::Indirect({:x})", ivn)
71+
}
72+
PcodeAddressLattice::Computed(sv) => {
73+
write!(f, "PcodeAddressLattice::Computed({:x})", sv)
6674
}
6775
PcodeAddressLattice::Top => write!(f, "PcodeAddressLattice::Top"),
6876
}
@@ -103,14 +111,21 @@ impl PartialOrd for PcodeAddressLattice {
103111
None
104112
}
105113
}
114+
(Self::Indirect(x), Self::Indirect(y)) => {
115+
if x == y {
116+
Some(Ordering::Equal)
117+
} else {
118+
None
119+
}
120+
}
106121
(Self::Computed(x), Self::Computed(y)) => {
107122
if x == y {
108123
Some(Ordering::Equal)
109124
} else {
110125
None
111126
}
112127
}
113-
// Different kinds (Const vs Computed) are incomparable
128+
// Different kinds are incomparable
114129
_ => None,
115130
}
116131
}
@@ -120,26 +135,24 @@ impl JoinSemiLattice for PcodeAddressLattice {
120135
fn join(&mut self, other: &Self) {
121136
// Match on references to avoid moving out of `self` while inspecting it.
122137
match (&*self, other) {
123-
(Self::Top, _) => *self = Self::Top,
124-
(_, Self::Top) => *self = Self::Top,
138+
(Self::Top, _) | (_, Self::Top) => *self = Self::Top,
125139
(Self::Const(a), Self::Const(b)) => {
126-
if a == b {
127-
// keep the same concrete value
128-
} else {
140+
if a != b {
129141
*self = Self::Top;
130142
}
131143
}
132-
(Self::Computed(x), Self::Computed(y)) => {
133-
if x == y {
134-
// keep the same computed descriptor
135-
} else {
144+
(Self::Indirect(x), Self::Indirect(y)) => {
145+
if x != y {
136146
*self = Self::Top;
137147
}
138148
}
139-
// Mixing Const and Computed -> unknown
140-
_ => {
141-
*self = Self::Top;
149+
(Self::Computed(x), Self::Computed(y)) => {
150+
if x != y {
151+
*self = Self::Top;
152+
}
142153
}
154+
// Mixing different kinds -> unknown
155+
_ => *self = Self::Top,
143156
};
144157
}
145158
}
@@ -161,15 +174,16 @@ impl AbstractState for PcodeAddressLattice {
161174
PcodeOperation::BranchInd { input }
162175
| PcodeOperation::CallInd { input }
163176
| PcodeOperation::Return { input } => {
164-
return once(PcodeAddressLattice::Computed(input.clone())).into();
177+
return once(PcodeAddressLattice::Indirect(input.clone())).into();
165178
}
166179
_ => {}
167180
}
168181

169182
match self {
170183
PcodeAddressLattice::Const(a) => a.transfer(op).into_iter().map(Self::Const).into(),
171-
PcodeAddressLattice::Computed(_) => empty().into(),
172-
PcodeAddressLattice::Top => empty().into(),
184+
PcodeAddressLattice::Indirect(_)
185+
| PcodeAddressLattice::Computed(_)
186+
| PcodeAddressLattice::Top => empty().into(),
173187
}
174188
}
175189
}
@@ -181,9 +195,9 @@ impl LocationState for PcodeAddressLattice {
181195
) -> Option<crate::analysis::pcode_store::PcodeOpRef<'a>> {
182196
match self {
183197
PcodeAddressLattice::Const(a) => t.get_pcode_op_at(a),
184-
// If the location is computed or top, we cannot directly get a concrete op
185-
PcodeAddressLattice::Computed(_) => None,
186-
PcodeAddressLattice::Top => None,
198+
PcodeAddressLattice::Indirect(_)
199+
| PcodeAddressLattice::Computed(_)
200+
| PcodeAddressLattice::Top => None,
187201
}
188202
}
189203

@@ -198,9 +212,8 @@ impl Display for PcodeAddressLattice {
198212
PcodeAddressLattice::Const(concrete_pcode_address) => {
199213
write!(f, "{:x}", concrete_pcode_address)
200214
}
201-
PcodeAddressLattice::Computed(indirect_var_node) => {
202-
write!(f, "{:x}", indirect_var_node)
203-
}
215+
PcodeAddressLattice::Indirect(ivn) => write!(f, "{}", ivn),
216+
PcodeAddressLattice::Computed(sv) => write!(f, "{}", sv),
204217
PcodeAddressLattice::Top => write!(f, "Top"),
205218
}
206219
}

jingle/src/analysis/location/basic/state.rs

Lines changed: 18 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ use std::{
22
borrow::Borrow,
33
cmp::Ordering,
44
fmt::{Display, LowerHex},
5+
hash::Hash,
56
iter::{empty, once},
67
};
78

@@ -16,7 +17,7 @@ use crate::{
1617
state::{AbstractState, LocationState, MergeOutcome, Successor},
1718
},
1819
location::basic::BasicLocationAnalysis,
19-
valuation::SimpleValuationState,
20+
valuation::{SimpleValuationState, SimpleValue},
2021
},
2122
modeling::machine::{MachineState, cpu::concrete::ConcretePcodeAddress},
2223
register_strengthen,
@@ -178,13 +179,20 @@ impl LocationState for BasicLocationState {
178179

179180
impl BasicLocationState {
180181
pub fn strengthen_from_valuation(&mut self, v: &SimpleValuationState) {
181-
if let PcodeAddressLattice::Computed(indirect_var_node) = &self.inner {
182-
let ptr_value = v.get_value(indirect_var_node.pointer_location());
183-
if let Some(value) = ptr_value {
184-
if let Some(v) = value.as_const_value() {
185-
self.inner = PcodeAddressLattice::Const(ConcretePcodeAddress::from(v as u64))
182+
if let PcodeAddressLattice::Indirect(ivn) = &self.inner {
183+
if let Some(value) = v.get_value(ivn.pointer_location()) {
184+
if matches!(value, SimpleValue::Top) {
185+
// Top carries no useful info; Indirect(ivn) is more informative.
186+
return;
187+
}
188+
if let Some(addr) = value.as_const_value() {
189+
self.inner =
190+
PcodeAddressLattice::Const(ConcretePcodeAddress::from(addr as u64));
191+
} else {
192+
self.inner = PcodeAddressLattice::Computed(value.clone());
186193
}
187194
}
195+
// No info → leave as Indirect (two paths with no valuation are genuinely equal)
188196
}
189197
}
190198
}
@@ -195,15 +203,17 @@ impl CfgState for BasicLocationState {
195203
fn new_const(&self, i: &jingle_sleigh::SleighArchInfo) -> Self::Model {
196204
match &self.inner {
197205
PcodeAddressLattice::Const(addr) => MachineState::fresh_for_address(i, *addr),
198-
// For computed or unknown locations, fall back to a generic fresh machine state.
199-
PcodeAddressLattice::Computed(_) | PcodeAddressLattice::Top => MachineState::fresh(i),
206+
PcodeAddressLattice::Indirect(_)
207+
| PcodeAddressLattice::Computed(_)
208+
| PcodeAddressLattice::Top => MachineState::fresh(i),
200209
}
201210
}
202211

203212
fn model_id(&self) -> String {
204213
match &self.inner {
205214
PcodeAddressLattice::Const(a) => a.model_id(),
206215
PcodeAddressLattice::Top => "State_Top_".to_string(),
216+
PcodeAddressLattice::Indirect(_) => "State_Indirect_".to_string(),
207217
PcodeAddressLattice::Computed(_) => "State_Computed_".to_string(),
208218
}
209219
}

jingle/src/analysis/location/bound/mod.rs

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,12 @@ use crate::modeling::machine::cpu::concrete::ConcretePcodeAddress;
1414
///
1515
/// Use the provided constructors to choose the desired configuration.
1616
pub struct BoundedBranchAnalysis {
17-
/// Optional maximum number of instructions to observe.
17+
/// Maximum number of ISA instructions.
1818
max_instructions: Option<usize>,
19-
/// Optional maximum number of branches to observe.
19+
/// Maximum number of explicit ISA branches.
2020
max_branches: Option<usize>,
21+
/// Maximum number of pcode steps
22+
max_ops: Option<usize>,
2123
}
2224

2325
impl BoundedBranchAnalysis {
@@ -26,6 +28,7 @@ impl BoundedBranchAnalysis {
2628
Self {
2729
max_instructions: None,
2830
max_branches: Some(max_branches),
31+
max_ops: None,
2932
}
3033
}
3134

@@ -34,15 +37,21 @@ impl BoundedBranchAnalysis {
3437
Self {
3538
max_instructions: Some(max_instructions),
3639
max_branches: None,
40+
max_ops: None,
3741
}
3842
}
3943

4044
/// Create an analysis with explicit optional bounds for instructions and branches.
4145
/// Use `None` for any bound you do not want to apply.
42-
pub fn with_bounds(max_instructions: Option<usize>, max_branches: Option<usize>) -> Self {
46+
pub fn with_bounds(
47+
max_instructions: Option<usize>,
48+
max_branches: Option<usize>,
49+
max_ops: Option<usize>,
50+
) -> Self {
4351
Self {
4452
max_instructions,
4553
max_branches,
54+
max_ops,
4655
}
4756
}
4857

@@ -55,6 +64,10 @@ impl BoundedBranchAnalysis {
5564
pub fn max_instructions(&self) -> Option<usize> {
5665
self.max_instructions
5766
}
67+
68+
pub fn max_ops(&self) -> Option<usize> {
69+
self.max_ops
70+
}
5871
}
5972

6073
impl ConfigurableProgramAnalysis for BoundedBranchAnalysis {
@@ -64,6 +77,6 @@ impl ConfigurableProgramAnalysis for BoundedBranchAnalysis {
6477

6578
impl IntoState<BoundedBranchAnalysis> for ConcretePcodeAddress {
6679
fn into_state(self, c: &BoundedBranchAnalysis) -> BoundedBranchState {
67-
BoundedBranchState::with_both_bounds(c.max_instructions, c.max_branches)
80+
BoundedBranchState::with_all_bounds(c.max_instructions, c.max_branches, c.max_ops)
6881
}
6982
}

0 commit comments

Comments
 (0)