Skip to content

Commit

Permalink
feat: search for reads of *any* register when building an initial `Sy…
Browse files Browse the repository at this point in the history
…mContext`
  • Loading branch information
alexkeizer committed Oct 1, 2024
1 parent 16e3f4f commit b95fe25
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 8 deletions.
20 changes: 19 additions & 1 deletion Tactics/Common.lean
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ def reflectPFLag (e : Expr) : MetaM PFlag :=

/-- Reflect a concrete `StateField` -/
def reflectStateField (e : Expr) : MetaM StateField :=
match_expr e with
match_expr e.consumeMData with
| StateField.GPR x => StateField.GPR <$> reflectBitVecLiteral _ x
| StateField.SFP x => StateField.SFP <$> reflectBitVecLiteral _ x
| StateField.PC => pure StateField.PC
Expand Down Expand Up @@ -259,6 +259,24 @@ def mkEqArmState (x y : Expr) : Expr :=
def mkEqReflArmState (x : Expr) : Expr :=
mkApp2 (.const ``Eq.refl [1]) mkArmState x

/-- Return `x = y` given expressions `x, y : StateField <field>` -/
def mkEqStateValue (field x y : Expr) : Expr :=
let ty := mkApp (mkConst ``state_value) field
mkApp3 (.const ``Eq [1]) ty x y

/-- Return `r <field> <state> = <value>` -/
def mkEqReadField (field state value : Expr) : Expr :=
let r := mkApp2 (mkConst ``r) field state
mkEqStateValue field r value

/-- If expression `e` is `r ?field ?state = ?value`, return
`some (field, state, value)`, else return `none` -/
def Lean.Expr.eqReadField? (e : Expr) : Option (Expr × Expr × Expr) := do
let (_ty, lhs, value) ← e.eq?
let_expr r field state := lhs
| none
some (field, state, value)

/-! ## Tracing helpers -/

def traceHeartbeats (cls : Name) (header : Option String := none) :
Expand Down
29 changes: 22 additions & 7 deletions Tactics/Sym/Context.lean
Original file line number Diff line number Diff line change
Expand Up @@ -305,7 +305,6 @@ private def withErrorContext (name : Name) (type? : Option Expr) (k : MetaM α)
| none => m!""
throwErrorAt e.getRef "{e.toMessageData}\n\nIn {h}{type}"

-- protected def AxEffects.searchFor

/-- Build the lazy search structure (for use with `searchLCtx`)
to populate the `SymContext` state from the local context.
Expand Down Expand Up @@ -406,13 +405,29 @@ protected def searchFor : SearchLCtxForM SymM Unit := do
})
)

/- TODO(@alexkeizer): search for any other hypotheses of the form
`r ?field <currentState> = _`, and record those.
Keeping in mind that we have to do this search AFTER `h_pc` or `h_err`, to
ensure those field-specific searches take priority.
Also, maybe for memory-reads as well? Or we can hold off on that untill
after the equality refactor -/
-- Find `r ?field currentState = ?value`
-- NOTE: this HAS to come after the search for specific fields, like `h_pc`,
-- or `h_err`, to ensure those take priority and the special handling
-- of those fields gets applied.
searchLCtxFor
(expectedType := do
let field ← mkFreshExprMVar (mkConst ``StateField)
let value ← mkFreshExprMVar none
return mkEqReadField field currentState value
)
(whenFound := fun decl ty => do
let some (field, _state, value) := ty.eqReadField?
| throwError "internal error: unexpected type:\n {ty}"

let field ← reflectStateField (← instantiateMVars field)
AxEffects.setFieldEffect field {
value := ←instantiateMVars value,
proof := decl.toExpr
}
return .continu
)
/- TODO(@alexkeizer): Should we search for memory as well?
Probably we can only do so after the memoryProof refactor -/
return ()

/-- Build a `SymContext` by searching the local context of the main goal for
Expand Down

0 comments on commit b95fe25

Please sign in to comment.