st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-03-11 18:47:08 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

add types to the analyzer

Browse source
This commit is contained in:
ProgramSnail 2026-02-23 15:25:20 +00:00
parent 7b312fcfdd
commit 04fb1da502
2 changed files with 39 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

36
simplest_model/analyzer.ml
View file

@ -37,59 +37,61 @@ struct
| ([], _) -> raise Not_found
let env_get state id = match state with
let env_get (state : state) (id : data) : data = match state with
(env, _mem, _mem_len, _assignments) -> List.assoc id env
let env_add state id mem_id = match state with
let env_add (state : state) (id : data) (mem_id : data) : state = match state with
(env, mem, mem_len, assignments) -> let env = (id, mem_id) :: env in
(env, mem, mem_len, assignments)
let inv_id mem_len id = mem_len - id - 1
let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
let mem_get state id = match state with
let mem_get (state : state) (id : data) : value = match state with
(_env, mem, mem_len, _assignments) -> List.nth mem @@ inv_id mem_len @@ env_get state id
let mem_set state id value= match state with
let mem_set (state : state) (id : data) (value : value) : state = match state with
(env, mem, mem_len, assignments) -> let mem_id = inv_id mem_len @@ env_get state id in
let mem = list_replace mem mem_id value in (env, mem, mem_len, id :: assignments)
let mem_add state value = match state with
let mem_add (state : state) (value : value) : state = match state with
(env, mem, mem_len, assignments) -> let mem = value :: mem in (env, mem, mem_len + 1, assignments)
let mem_check state id = if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
let mem_check (state : state) (id : data) : state =
if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
let arg_to_value state arg = match arg with
let arg_to_value (state : state) (arg : arg) : value = match arg with
| RValue -> UnitV
| LValue id -> mem_get state id
let st_mem_len state =
let st_mem_len (state : state) : int =
match state with (_, _, mem_len, _) -> mem_len
let st_add_arg state state_before id arg_tag arg =
let st_add_arg (state : state) (state_before : state)
(id : data) (arg_tag : tag) (arg : arg) : state =
match (arg_tag, arg) with
| (Ref, RValue) -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *)
| (Ref, LValue arg) -> env_add state id (env_get state_before arg)
| (Value, arg) -> let state = mem_add state (arg_to_value state_before arg) in
env_add state id (st_mem_len state - 1)
let st_spoil_assignments state =
let st_spoil_assignments (state : state) : state =
match state with (env, mem, mem_len, assignments) ->
(* TODO: use env var ids instead of mem_ids ?? *)
(env, List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments, mem_len, [])
let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
let rec eval_stmt state prog stmt =
let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state =
match stmt with
| Call (f_id, args) -> eval_fun state prog (List.nth prog f_id) (List.map (fun arg -> LValue arg) args)
| Read id -> mem_check state id
| Write id -> mem_set state id UnitV
and eval_body state prog body =
and eval_body (state : state) (prog : fun_decl list) (body : body) : state =
List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
and eval_fun state prog decl args =
and eval_fun (state : state) (prog : fun_decl list) (decl : fun_decl) (args : arg list) : state =
match decl with (arg_tags, body) ->
match state with (env_before, mem_before, len_before, assignments_before) as state_before ->
let state = ([], mem_before, len_before, []) in
@ -99,14 +101,14 @@ struct
match state with (_env, mem, len, _assignments) ->
(env_before, list_drop (len - len_before) mem, len_before, assignments_before) (* TODO: save some assignments ?? *)
and eval_fun_empty_args state prog decl =
and eval_fun_empty_args (state : state) (prog : fun_decl list) (decl : fun_decl) : state =
match decl with (arg_tags, _) ->
let args = List.map (fun _ -> RValue) arg_tags in
eval_fun state prog decl args
let empty_state = ([], [], 0, [])
let empty_state : state = ([], [], 0, [])
let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl
let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl
(* tests *)