mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-04-30 17:52:41 +00:00
structures: remove or comment old code in the analyzer
This commit is contained in:
ProgramSnail
parent
1c7f676a54
commit
ac67849c5d
1 changed files with 16 additions and 239 deletions
|
|
@ -342,250 +342,27 @@ struct
|
||||||
|
|
||||||
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
|
||||||
|
|
||||||
(* --- *)
|
|
||||||
|
|
||||||
let rec list_zip_with f xs ys = match xs, ys with (* TODO: alternative from stdlib *)
|
|
||||||
| x :: xs, y :: ys -> f x y :: list_zip_with f xs ys
|
|
||||||
| _, _ -> []
|
|
||||||
|
|
||||||
(* --- combination --- *)
|
|
||||||
|
|
||||||
let value_combine (left : value) (right : value) : value = match left, right with
|
|
||||||
| UnitV, UnitV -> UnitV
|
|
||||||
| BotV, BotV -> BotV
|
|
||||||
| _, _ -> UndefV (* NOTE: should be expanded in relational interpreter to not use ineq (?) *)
|
|
||||||
|
|
||||||
let memory_combine (left : value list) (right : value list) : value list =
|
|
||||||
list_zip_with value_combine left right
|
|
||||||
|
|
||||||
let state_combine (left : state) (right : state) : state = match left, right with
|
|
||||||
(lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) ->
|
|
||||||
if lenv != renv || lmem_len != rmem_len then raise Incompatible_states
|
|
||||||
else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited)
|
|
||||||
(* TODO: union visited lists instead ? *)
|
|
||||||
|
|
||||||
(* --- tag accessors --- *)
|
|
||||||
|
|
||||||
let is_read (tag : tag) : bool = match tag with
|
|
||||||
| (Rd, _, _, _, _) -> true
|
|
||||||
| _ -> false
|
|
||||||
|
|
||||||
let is_always_write (tag : tag) : bool = match tag with
|
|
||||||
| (_, AlwaysWr, _, _, _) -> true
|
|
||||||
| _ -> false
|
|
||||||
|
|
||||||
let is_may_write (tag : tag) : bool = match tag with
|
|
||||||
| (_, AlwaysWr, _, _, _) -> true
|
|
||||||
| (_, MayWr, _, _, _) -> true
|
|
||||||
| _ -> false
|
|
||||||
|
|
||||||
let is_never_write (tag : tag) : bool = match tag with
|
|
||||||
| (_, NeverWr, _, _, _) -> true
|
|
||||||
| _ -> false
|
|
||||||
|
|
||||||
let is_copy (tag : tag) : bool = match tag with
|
|
||||||
| (_, _, Cp, _, _) -> true
|
|
||||||
| _ -> false
|
|
||||||
|
|
||||||
let is_in (tag : tag) : bool = match tag with
|
|
||||||
| (_, _, _, In, _) -> true
|
|
||||||
| _ -> false
|
|
||||||
|
|
||||||
let is_out (tag : tag) : bool = match tag with
|
|
||||||
| (_, _, _, _, Out) -> true
|
|
||||||
| _ -> false
|
|
||||||
|
|
||||||
(* --- *)
|
|
||||||
|
|
||||||
let rec list_replace xs id value = match (xs, id) with
|
|
||||||
| (_x :: xs, 0) -> value :: xs
|
|
||||||
| (x :: xs, _n) -> x :: list_replace xs (id - 1) value
|
|
||||||
| ([], _) -> raise Not_found
|
|
||||||
|
|
||||||
let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
|
|
||||||
|
|
||||||
(* --- path accessors --- *)
|
|
||||||
|
|
||||||
let rec pathtype (t : argtype) (p : path) : argtype = match t, p with
|
|
||||||
| t, VarP x -> t
|
|
||||||
| RefT (tag, t), DerefP p -> pathtype t p
|
|
||||||
| TupleT ts, AccessP (p, n) -> pathtype (List.nth ts n) p
|
|
||||||
| _, _ -> raise Incompatible_path_and_type
|
|
||||||
|
|
||||||
let rec pathmem (m : argmem) (p : path) : data = match m, p with
|
|
||||||
| VarM m, VarP x -> m
|
|
||||||
| RefM m, DerefP p -> pathmem m p
|
|
||||||
| TupleM ms, AccessP (p, n) -> pathmem (List.nth ms n) p
|
|
||||||
| _, _ -> raise Incompatible_path_and_mem
|
|
||||||
|
|
||||||
let rec pathtag (t : argtype) (p : path) : tag = match t, p with
|
|
||||||
| RefT (tag, t), VarP x -> tag
|
|
||||||
| RefT (tag, t), DerefP p -> pathtag t p
|
|
||||||
| TupleT ts, AccessP (p, n) -> pathtag (List.nth ts n) p
|
|
||||||
| _, _ -> raise Incompatible_path_and_type_for_tag
|
|
||||||
|
|
||||||
let rec pathvar (p : path) : data = match p with
|
|
||||||
| VarP x -> x
|
|
||||||
| DerefP p -> pathvar p
|
|
||||||
| AccessP (p, n) -> pathvar p
|
|
||||||
|
|
||||||
let typeof (env : env) (p : path) : argtype = pathtype (snd (List.assoc (pathvar p) env)) p
|
|
||||||
let accessmem (env : env) (p : path) : data = pathmem (fst (List.assoc (pathvar p) env)) p
|
|
||||||
let argtag (env : env) (p : path) : tag = pathtag (snd (List.assoc (pathvar p) env)) p
|
|
||||||
(* TODO: check indices *)
|
|
||||||
let access_get (env : env) (mem : value list) (mem_len : data) (p : path) : value = List.nth mem @@ inv_id mem_len @@ accessmem env p
|
|
||||||
let access_set (env : env) (mem : value list) (mem_len : data) (p : path) (value : value) : value list = list_replace mem (inv_id mem_len @@ accessmem env p) value
|
|
||||||
|
|
||||||
(* --- *)
|
|
||||||
|
|
||||||
let visited_add (state : state) (id : data) : state =
|
|
||||||
match state with (env, mem, mem_len, visited) -> (env, mem, mem_len, id :: visited)
|
|
||||||
|
|
||||||
let visited_check (state : state) (id : data) : bool =
|
|
||||||
match state with (_, _, _, visited) -> List.exists (fun i -> i == id) visited
|
|
||||||
|
|
||||||
(* --- *)
|
|
||||||
|
|
||||||
(* TODO: replacewith more useful path versions *)
|
|
||||||
let env_get (state : state) (id : data) : (argmem * argtype) =
|
|
||||||
match state with (env, _mem, _mem_len, _visited) -> List.assoc id env
|
|
||||||
|
|
||||||
let env_add (state : state) (id : data) (argmem : argmem) (argtype : argtype) : state = match state with
|
|
||||||
(env, mem, mem_len, visited) -> let env = (id, (argmem, argtype)) :: env in
|
|
||||||
(env, mem, mem_len, visited)
|
|
||||||
|
|
||||||
let mem_get (state : state) (p : path) : value = match state with
|
|
||||||
(env, mem, mem_len, _visited) -> access_get env mem mem_len p
|
|
||||||
|
|
||||||
let mem_set (state : state) (p : path) (value : value) : state = match state with
|
|
||||||
(env, mem, mem_len, visited) -> (env, access_set env mem mem_len p value, mem_len, visited)
|
|
||||||
|
|
||||||
let mem_add (state : state) (value : value) : state = match state with
|
|
||||||
(env, mem, mem_len, visited) -> let mem = value :: mem in (env, mem, mem_len + 1, visited)
|
|
||||||
|
|
||||||
let mem_check (state : state) (p : path) : unit =
|
|
||||||
(* TODO: use path in error instead *)
|
|
||||||
if mem_get state p == BotV then raise @@ Incorrect_memory_access (pathvar p) else ()
|
|
||||||
|
|
||||||
(* --- *)
|
|
||||||
|
|
||||||
let arg_to_value (state : state) (arg : arg) : value = match arg with
|
|
||||||
| RValue -> UnitV
|
|
||||||
| LValue p -> mem_get state p
|
|
||||||
(* TODO: FIXME: args as argmem ?? *)
|
|
||||||
|
|
||||||
let st_mem_len (state : state) : int =
|
|
||||||
match state with (_, _, mem_len, _) -> mem_len
|
|
||||||
|
|
||||||
let check_tag_correct (tag : tag) (id : data) : unit =
|
|
||||||
if (* (is_in tag && not (is_read tag)) || *) (* TODO: required ?? *)
|
|
||||||
is_out tag > is_always_write tag ||
|
|
||||||
is_read tag > is_in tag
|
|
||||||
(* || is_copy tag && is_out tag *) (* ?? *)
|
|
||||||
then raise @@ Invalid_argument_tag id
|
|
||||||
else ()
|
|
||||||
|
|
||||||
let st_add_arg (state : state) (state_before : state)
|
|
||||||
(id : data) (arg_tag : tag) (arg : arg) : state =
|
|
||||||
check_tag_correct arg_tag id;
|
|
||||||
if is_copy arg_tag
|
|
||||||
then let state = mem_add state (arg_to_value state_before arg) in
|
|
||||||
env_add state id arg_tag (st_mem_len state - 1)
|
|
||||||
else match arg with
|
|
||||||
| RValue -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *)
|
|
||||||
| LValue arg -> let (parent_tag, mem_id) = env_get state_before arg in
|
|
||||||
if is_may_write arg_tag > is_always_write parent_tag (* TODO: FIXME: not updated semantics ?? *)
|
|
||||||
then raise @@ Incorrect_const_cast id
|
|
||||||
else if is_read arg_tag
|
|
||||||
then env_add state id arg_tag mem_id
|
|
||||||
(* TODO: parent state is spoiled, check that this is correct *)
|
|
||||||
else let state_ext = env_add state id arg_tag mem_id in
|
|
||||||
mem_set state_ext id BotV
|
|
||||||
|
|
||||||
(* TODO: FIXME: not enough tests on incorrect const cast (passed without ref or out 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 =
|
|
||||||
match state with (env, mem, mem_len, _visited) ->
|
|
||||||
let state_before = state in
|
|
||||||
let spoil_folder (state : state) (tag : tag) (id : data) : state =
|
|
||||||
let parent_tag = fst (env_get state id) in
|
|
||||||
(* NOTE: replaced with later condition *)
|
|
||||||
(* if is_write tag > is_write parent_tag && (not (is_copy tag) || is_out tag) then raise @@ Incorrect_const_cast idi else *)
|
|
||||||
let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *)
|
|
||||||
in if is_never_write tag then state (* TODO: FIXME: check *)
|
|
||||||
else match is_out tag with
|
|
||||||
| true -> if not @@ is_always_write parent_tag then raise @@ Incorrect_const_cast id
|
|
||||||
else mem_set state id UnitV
|
|
||||||
| false -> if is_copy tag then state
|
|
||||||
else if not @@ is_may_write parent_tag then raise @@ Incorrect_const_cast id (* TODO: check that may modifier correct *)
|
|
||||||
else mem_set state id BotV
|
|
||||||
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 rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state =
|
|
||||||
match stmt with
|
|
||||||
| Call (f_id, args) -> let (arg_tags, _) as f_decl = List.nth prog f_id in
|
|
||||||
let state_with_visited = if visited_check state f_id
|
|
||||||
then state
|
|
||||||
else let new_state_with_visited = visited_add state f_id 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 *)
|
|
||||||
state_fun
|
|
||||||
in st_spoil_by_args state_with_visited arg_tags args
|
|
||||||
| Read id -> mem_check state id; state
|
|
||||||
| Write id -> if is_may_write @@ fst @@ env_get state id
|
|
||||||
then mem_set state id UnitV
|
|
||||||
else raise @@ Incorrect_const_cast id
|
|
||||||
| Choice (xs, ys) -> let state_x = eval_body state prog xs in
|
|
||||||
let state_y = eval_body state prog ys in
|
|
||||||
state_combine state_x state_y
|
|
||||||
(* TODO: FIXME: additional may write / always write checks ?? *)
|
|
||||||
|
|
||||||
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 : 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, visited_before) as state_before ->
|
|
||||||
let state : state = ([], mem_before, len_before, visited_before) in
|
|
||||||
let (state, _) = List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state_before id arg_tag arg, id + 1))
|
|
||||||
(state, 0) arg_tags args in
|
|
||||||
let state = eval_body state prog body in
|
|
||||||
match state with (_env, mem, len, visited) ->
|
|
||||||
(env_before, mem_before, len_before, visited)
|
|
||||||
(* (env_before, list_drop (len - len_before) mem, len_before, visited) (* TODO: save some assignments ?? *) *)
|
|
||||||
|
|
||||||
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 : state = ([], [], 0, [])
|
|
||||||
|
|
||||||
let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl
|
|
||||||
|
|
||||||
(* tests *)
|
(* tests *)
|
||||||
|
|
||||||
let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut)
|
(* let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut) *)
|
||||||
let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut)
|
(* let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut) *)
|
||||||
let ri_value : tag = (Rd, NeverWr, Cp, In, NOut)
|
(* let ri_value : tag = (Rd, NeverWr, Cp, In, NOut) *)
|
||||||
let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut)
|
(* let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut) *)
|
||||||
let mwi_value : tag = (NRd, MayWr, Cp, In, NOut)
|
(* let mwi_value : tag = (NRd, MayWr, Cp, In, NOut) *)
|
||||||
let i_value : tag = (NRd, NeverWr, Cp, In, NOut)
|
(* let i_value : tag = (NRd, NeverWr, Cp, In, NOut) *)
|
||||||
let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut)
|
(* let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut) *)
|
||||||
let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut)
|
(* let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut) *)
|
||||||
let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut)
|
(* let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut) *)
|
||||||
let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut)
|
(* let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut) *)
|
||||||
let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut)
|
(* let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut) *)
|
||||||
let i_ref : tag = (NRd, NeverWr, Rf, In, NOut)
|
(* let i_ref : tag = (NRd, NeverWr, Rf, In, NOut) *)
|
||||||
|
|
||||||
(* >> tests without functions *)
|
(* >> tests without functions *)
|
||||||
|
|
||||||
let%expect_test "empty" =
|
(* let%expect_test "empty" = *)
|
||||||
eval_prog ([], ([], []));
|
(* eval_prog ([], ([], [])); *)
|
||||||
Printf.printf "done!";
|
(* Printf.printf "done!"; *)
|
||||||
[%expect {| done! |}]
|
(* [%expect {| done! |}] *)
|
||||||
|
|
||||||
(* let%expect_test "ref param in main failure" = *)
|
(* let%expect_test "ref param in main failure" = *)
|
||||||
(* try (eval_prog ([], ([i_ref], [])); *)
|
(* try (eval_prog ([], ([i_ref], [])); *)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue