Skip to content

Unify observation type name, add arm8 obs model #209

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
palmskog merged 3 commits into from
Nov 10, 2025
Merged

Unify observation type name, add arm8 obs model #209

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a1993a8
basic SCAM-V instrumentation of observations for arm8 incr program
palmskog Nov 4, 2025
913d86e
use 'obs_type everywhere instead of sometimes 'observation_type
palmskog Nov 4, 2025
c912b55
polishing of arm8 observation examples
palmskog Nov 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions examples/arm8/incr/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLBADIR)/src/tools/backlifter \
$(HOLBADIR)/src/tools/symbexec \
$(HOLBADIR)/src/tools/symbexec/examples/common \
$(HOLBADIR)/src/tools/scamv/obsmodel \
$(HOLBADIR)/src

all: $(DEFAULT_TARGETS)
Expand Down
35 changes: 35 additions & 0 deletions examples/arm8/incr/incr_obsScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
open HolKernel boolLib Parse bossLib;

open bir_obs_modelLib;

open bslSyntax;

open incrTheory;

val _ = new_theory "incr_obs";

val mem_bounds =
let
open wordsSyntax;
val (mem_base, mem_len) = (Arbnum.fromHexString "0xFFCC0000",
Arbnum.fromHexString "0x10000");
val mem_end = (Arbnum.- (Arbnum.+ (mem_base, mem_len), Arbnum.fromInt 128));
in
pairSyntax.mk_pair
(mk_wordi (mem_base, 64),
mk_wordi (mem_end, 64))
end;

val bir_incr_obs_prog =
let
val prog_tm = (snd o dest_eq o concl) bir_incr_prog_def;
val om = get_obs_model "mem_address_pc";
in
(#add_obs om) mem_bounds (proginst_fun_gen (#obs_hol_type om) prog_tm)
end;

Definition bir_incr_obs_prog_def:
bir_incr_obs_prog = ^bir_incr_obs_prog
End

val _ = export_theory ();
1 change: 1 addition & 0 deletions examples/arm8/swap/Holmakefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
$(HOLBADIR)/src/tools/backlifter \
$(HOLBADIR)/src/tools/symbexec \
$(HOLBADIR)/src/tools/symbexec/examples/common \
$(HOLBADIR)/src/tools/scamv/obsmodel \
$(HOLBADIR)/src

all: $(DEFAULT_TARGETS)
Expand Down
35 changes: 35 additions & 0 deletions examples/arm8/swap/swap_obsScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
open HolKernel boolLib Parse bossLib;

open bir_obs_modelLib;

open bslSyntax;

open swapTheory;

val _ = new_theory "swap_obs";

val mem_bounds =
let
open wordsSyntax;
val (mem_base, mem_len) = (Arbnum.fromHexString "0xFFCC0000",
Arbnum.fromHexString "0x10000");
val mem_end = (Arbnum.- (Arbnum.+ (mem_base, mem_len), Arbnum.fromInt 128));
in
pairSyntax.mk_pair
(mk_wordi (mem_base, 64),
mk_wordi (mem_end, 64))
end;

val bir_swap_obs_prog =
let
val prog_tm = (snd o dest_eq o concl) bir_swap_prog_def;
val om = get_obs_model "mem_address_pc";
in
(#add_obs om) mem_bounds (proginst_fun_gen (#obs_hol_type om) prog_tm)
end;

Definition bir_swap_obs_prog_def:
bir_swap_obs_prog = ^bir_swap_obs_prog
End

val _ = export_theory ();
6 changes: 3 additions & 3 deletions examples/riscv/test-riscv.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ val _ = print_and_check_thm
``
bir_is_lifted_prog riscv_bmr (WI_end (0x10488w : word64) (0x104A8w : word64))
bir_swap_progbin
(bir_swap_prog : 'observation_type bir_program_t)
(bir_swap_prog : 'obs_type bir_program_t)
``;

val _ = print_and_check_thm
Expand Down Expand Up @@ -67,7 +67,7 @@ val _ = print_and_check_thm
``
bir_is_lifted_prog riscv_bmr (WI_end (0x10488w : word64) (0x10498w : word64))
bir_incr_progbin
(bir_incr_prog : 'observation_type bir_program_t)
(bir_incr_prog : 'obs_type bir_program_t)
``;

val _ = print_and_check_thm
Expand Down Expand Up @@ -98,7 +98,7 @@ val _ = print_and_check_thm
``
bir_is_lifted_prog riscv_bmr (WI_end (0x10488w : word64) (0x10498w : word64))
bir_mod2_progbin
(bir_mod2_prog : 'observation_type bir_program_t)
(bir_mod2_prog : 'obs_type bir_program_t)
``;

val _ = print_and_check_thm
Expand Down
2 changes: 1 addition & 1 deletion examples/tutorial/7-composition/test-composition.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ val _ = print_and_check_thm
bir_add_reg_ct
``
bir_cont
(bir_add_reg_prog:'observation_type bir_program_t)
(bir_add_reg_prog:'obs_type bir_program_t)
bir_exp_true
(BL_Address (Imm64 28w))
{BL_Address (Imm64 72w)} EMPTY bir_add_reg_contract_1_pre
Expand Down
2 changes: 1 addition & 1 deletion src/tools/cfg/examples/test-collections.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ val bir_blocks = [
(Arbnum.fromHexString "8166",
``<|bb_label :=
BL_Address_HC (Imm32 (33126w :word32)) "E004 (b.n 8172 <main+0x6e>)";
bb_statements := ([] :'observation_type bir_stmt_basic_t list);
bb_statements := ([] :'obs_type bir_stmt_basic_t list);
bb_last_statement :=
BStmt_Jmp (BLE_Label (BL_Address (Imm32 (33138w :word32))))|>``)
];
Expand Down
2 changes: 1 addition & 1 deletion src/tools/comp/bir_compositionLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -510,7 +510,7 @@ open bir_inst_liftingHelpersLib;
[bir_bool_expTheory.bir_is_bool_exp_env_def, bir_tsTheory.bir_ts_def, bir_tsTheory.bir_weak_trs_def] >>
Cases_on `bir_exec_to_labels
(^(pred_setSyntax.mk_set [start_label]) UNION (^ilist))
(bir_add_reg_prog:'observation_type bir_program_t) s` >> (
(bir_add_reg_prog:'obs_type bir_program_t) s` >> (
FULL_SIMP_TAC (std_ss++HolBACoreSimps.holBACore_ss) [bir_programTheory.bir_exec_to_labels_def]
) >>
IMP_RES_TAC bir_program_env_orderTheory.bir_exec_to_labels_n_ENV_ORDER >>
Expand Down
2 changes: 1 addition & 1 deletion src/tools/lifter/bir_inst_liftingHelpersLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ val bir_assert_desc_t_ty =

val bir_updateE_desc_exp_tm = prim_mk_const{Name="bir_updateE_desc_exp", Thy="bir_update_block"}

val block_observe_ty = mk_vartype "'observation_type"
val block_observe_ty = mk_vartype "'obs_type"

val bir_is_lifted_inst_block_COMPUTE_block_tm =
inst [Type.alpha |-> block_observe_ty] (get_const "bir_is_lifted_inst_block_COMPUTE_block")
Expand Down
5 changes: 1 addition & 4 deletions src/tools/scamv/proggen/bir_prog_genLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,11 +62,8 @@ struct
val prog_range = da_sections_minmax sections;
val (thm_prog, errors) = bmil_bir_lift_prog_gen prog_range sections;
val lifted_prog = (snd o dest_comb o concl) thm_prog;
val lifted_prog_typed =
inst [Type`:'observation_type` |-> Type`:'obs_type`]
lifted_prog;
in
lifted_prog_typed
lifted_prog
end

fun process_asm_code asm_code =
Expand Down
2 changes: 1 addition & 1 deletion src/tools/scamv/symbexec/bir_symb_execLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ fun symb_exec_run max bp pd st =

(* Given a Program, exec until every branch halts *)
(*
val bir_program = ``BirProgram [] : 'observation_type bir_program_t``;
val bir_program = ``BirProgram [] : 'obs_type bir_program_t``;

val bir_program = ``BirProgram
[<|bb_label := BL_Address_HC (Imm64 0w) "F9400023 (ldr x3, [x1])";
Expand Down
8 changes: 4 additions & 4 deletions src/tools/symbexec/bir_symbLib.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ fun bir_symb_transfer
val birs_state_thm = REWRITE_CONV [birenvtyl_EVAL_thm] birs_state_init_pre_tm;

val birs_symb_symbols_f_sound_prog_thm =
(SPEC (inst [Type`:'observation_type` |-> Type.alpha] bprog_tm)
(SPEC (inst [Type`:'obs_type` |-> Type.alpha] bprog_tm)
bir_symb_soundTheory.birs_symb_symbols_f_sound_thm);

val birs_prop_transfer_thm =
Expand Down Expand Up @@ -314,7 +314,7 @@ fun bir_symb_transfer
`\l. if l = ^bir_end_lbl_tm
then ^bspec_post_tm
else bir_exp_false`
] o SPEC bprog_tm o INST_TYPE [Type.alpha |-> Type`:'observation_type`])
] o SPEC bprog_tm o INST_TYPE [Type.alpha |-> Type`:'obs_type`])
abstract_jgmt_rel_bir_cont) >>
rw [] >>
METIS_TAC [abstract_jgmt_rel_thm]);
Expand Down Expand Up @@ -440,7 +440,7 @@ fun bir_symb_transfer_two
REWRITE_CONV [birenvtyl_EVAL_thm] birs_state_init_pre_tm;

val birs_symb_symbols_f_sound_prog_thm =
(SPEC (inst [Type`:'observation_type` |-> Type.alpha] bprog_tm)
(SPEC (inst [Type`:'obs_type` |-> Type.alpha] bprog_tm)
bir_symb_soundTheory.birs_symb_symbols_f_sound_thm);

val birs_prop_transfer_thm =
Expand Down Expand Up @@ -654,7 +654,7 @@ fun bir_symb_transfer_two
`\l. if l = BL_Address (Imm64 ^end_addr_1_tm) then ^bspec_post_1_tm
else if l = BL_Address (Imm64 ^end_addr_2_tm) then ^bspec_post_2_tm
else bir_exp_false`
] o SPEC bprog_tm o INST_TYPE [Type.alpha |-> Type`:'observation_type`])
] o SPEC bprog_tm o INST_TYPE [Type.alpha |-> Type`:'obs_type`])
abstract_jgmt_rel_bir_cont) >>
rw [] >>
METIS_TAC [abstract_jgmt_rel_thm]);
Expand Down
2 changes: 1 addition & 1 deletion src/tools/symbexec/examples/analysis/bir_program_transf_exampleScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -307,7 +307,7 @@ ASSUME_TAC
FULL_SIMP_TAC std_ss [pre_bir_nL_def, bir_programTheory.bir_state_is_terminated_def]
) >>

`MEM (BL_Address (Imm32 ^bir_frag_l_ml_tm)) (bir_labels_of_program (bprog:'observation_type bir_program_t))` by (
`MEM (BL_Address (Imm32 ^bir_frag_l_ml_tm)) (bir_labels_of_program (bprog:'obs_type bir_program_t))` by (
EVAL_TAC
) >>
FULL_SIMP_TAC std_ss [] >>
Expand Down
4 changes: 2 additions & 2 deletions src/tools/symbexec/examples/analysis/motorfunc_transfScript.sml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ End

(* prepare property transfer theorem *)
val birs_symb_symbols_f_sound_prog_thm =
(SPEC (inst [Type`:'observation_type` |-> Type.alpha] bprog) bir_symb_soundTheory.birs_symb_symbols_f_sound_thm);
(SPEC (inst [Type`:'obs_type` |-> Type.alpha] bprog) bir_symb_soundTheory.birs_symb_symbols_f_sound_thm);

val birs_prop_transfer_thm =
(MATCH_MP symb_prop_transferTheory.symb_prop_transfer_thm birs_symb_symbols_f_sound_prog_thm);
Expand Down Expand Up @@ -792,7 +792,7 @@ ASSUME_TAC
FULL_SIMP_TAC std_ss [pre_bir_nL_def, bir_programTheory.bir_state_is_terminated_def]
) >>

`MEM (BL_Address (Imm32 ^bir_frag_l_ml_tm)) (bir_labels_of_program (bprog:'observation_type bir_program_t))` by (
`MEM (BL_Address (Imm32 ^bir_frag_l_ml_tm)) (bir_labels_of_program (bprog:'obs_type bir_program_t))` by (
EVAL_TAC
) >>
FULL_SIMP_TAC std_ss [] >>
Expand Down