st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-03-12 02:57:09 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: st:607743a66f1ff1b470ad2c6a52ce65b9872dc4bf
Branches Tags
st:main
...
compare: st:bfe3d8dc92d9b489768ae3c5af1cee2129f55469
Branches Tags
st:main

2 commits
607743a66f ... bfe3d8dc92

Author SHA1 Message Date
ProgramSnail
bfe3d8dc92 simplest_model_with_mod: remove commented spoil arg, refactor state' 2026-03-03 17:29:48 +00:00
ProgramSnail
c2374d198d simplest_model_with_mod: wrong spoil arg function variant (commented) 2026-03-03 17:26:10 +00:00
1 changed files with 8 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

23
simplest_model_with_mods/analyzer_cap.ml
View file

@ -131,24 +131,23 @@ struct
else let state_ext = env_add state id arg_tag mem_id in else let state_ext = env_add state id arg_tag mem_id in
mem_set state_ext id BotV mem_set state_ext id BotV
(* TODO: use state_before ?? or state in some order (both orders ?, mod and then check ?) *) (* TODO; FIXME: forbid duplicates, collect lists of all spoils & checks ? *)
let st_spoil_by_args (state : state) (arg_tags : tag list) (args : data list) : state = let st_spoil_by_args (state : state) (arg_tags : tag list) (args : data list) : state =
match state with (env, mem, mem_len, _visited) -> match state with (env, mem, mem_len, _visited) ->
let state_before = state in let state_before = state in
let spoil_folder (state : state) (tag : tag) (id : data) : state = let spoil_folder (state : state) (tag : tag) (id : data) : state =
let parent_tag = fst (env_get state id) in let parent_tag = fst (env_get state id) in
if is_write tag > is_write parent_tag then raise @@ Incorrect_const_cast id if is_write tag > is_write parent_tag then raise @@ Incorrect_const_cast id
else let state' = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *) else let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *)
in if not @@ is_write tag then state' in if not @@ is_write tag then state
else match is_out tag with else match is_out tag with
| true -> mem_set state' id UnitV | true -> mem_set state id UnitV
| false -> if is_copy tag then state' | false -> if is_copy tag then state
else mem_set state' id BotV else mem_set state id BotV
in List.fold_left2 spoil_folder state arg_tags args in List.fold_left2 spoil_folder state arg_tags args
let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
(* TODO: FIXME: require at least one read / write for read / write args ?? *)
let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state = let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state =
match stmt with match stmt with
| Call (f_id, args) -> let (arg_tags, _) as f_decl = List.nth prog f_id in | Call (f_id, args) -> let (arg_tags, _) as f_decl = List.nth prog f_id in
@ -158,14 +157,8 @@ struct
let state_fun = eval_fun new_state_with_visited prog f_decl (List.map (fun arg -> LValue arg) args) in let state_fun = eval_fun new_state_with_visited prog f_decl (List.map (fun arg -> LValue arg) args) in
(* NOTE: now memory in function is not spoiled *) (* NOTE: now memory in function is not spoiled *)
state_fun state_fun
in in st_spoil_by_args state_with_visited arg_tags args
(* let state_checked = List.fold_left2 (fun s arg arg_tag -> *) | Read id -> mem_check state id; state
(* if is_read arg_tag *)
(* then mem_check s arg *)
(* else s) *)
(* state_with_visited args arg_tags in *)
st_spoil_by_args state_with_visited arg_tags args
| Read id -> mem_check state id
| Write id -> if is_write @@ fst @@ env_get state id | Write id -> if is_write @@ fst @@ env_get state id
then mem_set state id UnitV then mem_set state id UnitV
else raise @@ Incorrect_const_cast id else raise @@ Incorrect_const_cast id