Skip to content

Commit 6fdc296

Browse files
sim642sim642
committed
Lahenda domain praktikumis
1 parent 4bee347 commit 6fdc296

File tree

3 files changed

+30
-52
lines changed

3 files changed

+30
-52
lines changed

‎src/abseval/abseval.ml

Lines changed: 7 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,8 @@ struct
2929
let rec eval_guard (env: ED.t) (expr: expr) (branch: bool): ED.t =
3030
let expr_value = eval_expr env expr in
3131
let zero = ID.of_int 0 in
32-
if branch && ID.leq expr_value zero ||
33-
not branch && not (ID.leq zero expr_value) then
32+
if branch && ID.leq expr_value zero ||
33+
not branch && not (ID.leq zero expr_value) then
3434
ED.bot
3535
else
3636
match expr, branch with
@@ -66,48 +66,10 @@ struct
6666
let f_post_env = eval_stmt f_refined_env f in
6767
ED.join t_post_env f_post_env
6868
| While (c, b) ->
69-
let b_refined_env = eval_guard env c true in
70-
let b_post_env = eval_stmt b_refined_env b in
71-
let while_result = ED.join env b_post_env in
72-
73-
let b_refined_env = eval_guard while_result c true in
74-
let b_post_env = eval_stmt b_refined_env b in
75-
let while_result = ED.join while_result b_post_env in
76-
let b_refined_env = eval_guard while_result c true in
77-
let b_post_env = eval_stmt b_refined_env b in
78-
let while_result = ED.join while_result b_post_env in
79-
let b_refined_env = eval_guard while_result c true in
80-
let b_post_env = eval_stmt b_refined_env b in
81-
let while_result = ED.join while_result b_post_env in
82-
let b_refined_env = eval_guard while_result c true in
83-
let b_post_env = eval_stmt b_refined_env b in
84-
let while_result = ED.join while_result b_post_env in
85-
let b_refined_env = eval_guard while_result c true in
86-
let b_post_env = eval_stmt b_refined_env b in
87-
let while_result = ED.join while_result b_post_env in
88-
let b_refined_env = eval_guard while_result c true in
89-
let b_post_env = eval_stmt b_refined_env b in
90-
let while_result = ED.join while_result b_post_env in
91-
let b_refined_env = eval_guard while_result c true in
92-
let b_post_env = eval_stmt b_refined_env b in
93-
let while_result = ED.join while_result b_post_env in
94-
let b_refined_env = eval_guard while_result c true in
95-
let b_post_env = eval_stmt b_refined_env b in
96-
let while_result = ED.join while_result b_post_env in
97-
let b_refined_env = eval_guard while_result c true in
98-
let b_post_env = eval_stmt b_refined_env b in
99-
let while_result = ED.join while_result b_post_env in
100-
let b_refined_env = eval_guard while_result c true in
101-
let b_post_env = eval_stmt b_refined_env b in
102-
let while_result = ED.join while_result b_post_env in
103-
let b_refined_env = eval_guard while_result c true in
104-
let b_post_env = eval_stmt b_refined_env b in
105-
let while_result = ED.join while_result b_post_env in
106-
let b_refined_env = eval_guard while_result c true in
107-
let b_post_env = eval_stmt b_refined_env b in
108-
let while_result = ED.join while_result b_post_env in
109-
let b_refined_env = eval_guard while_result c true in
110-
let b_post_env = eval_stmt b_refined_env b in
111-
let while_result = ED.join while_result b_post_env in
69+
let f env' =
70+
let b_refined_env = eval_guard env' c true in
71+
eval_stmt b_refined_env b
72+
in
73+
let while_result = EDFP.closure f env in
11274
eval_guard while_result c false
11375
end

‎src/domain/intDomain.ml

Lines changed: 21 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -44,14 +44,27 @@ struct
4444
include Domain.Flat (struct type t = int [@@deriving eq, ord, show] end)
4545
let of_int i = Lift i
4646
let of_interval ((l, u): int * int): t =
47-
failwith "TODO"
47+
if l = u then
48+
Lift l
49+
else
50+
Top
4851

4952
(** Vihje: Eval.Concrete.eval_binary. *)
5053
let eval_binary (i1: t) (b: Ast.binary) (i2: t): t =
51-
failwith "TODO"
54+
match i1, i2 with
55+
| Bot, _
56+
| _, Bot -> Bot
57+
| Lift i1, Lift i2 -> Lift (Eval.Concrete.eval_binary i1 b i2)
58+
| Top, _
59+
| _, Top -> Top
5260

5361
let exclude (i: int) (i': t): t =
54-
failwith "TODO"
62+
match i' with
63+
| Bot -> Bot
64+
| Lift i' when i = i' -> Bot
65+
| Lift i' -> Lift i'
66+
| Top -> Top
67+
(* | _ -> i' *)
5568
end
5669

5770
(** Intervallide domeen. *)
@@ -65,14 +78,16 @@ struct
6578
let show = Format.asprintf "%a" pp
6679

6780
let leq ((l1, u1): t) ((l2, u2): t): bool =
68-
failwith "TODO"
81+
l2 <= l1 && u1 <= u2
6982

7083
let join ((l1, u1): t) ((l2, u2): t): t =
71-
failwith "TODO"
84+
(min l1 l2, max u1 u2)
7285

7386
let eval_binary ((l1, u1): t) (b: Ast.binary) ((l2, u2): t): t =
7487
match b with
75-
88+
| Add -> (l1 + l2, u1 + u2)
89+
| Lt when u1 < l2 -> (1, 1)
90+
| Lt when u2 <= l1 -> (0, 0)
7691
| Eq | Ne | Lt | Le | Gt | Ge -> (0, 1) (* Võrdluse tulemus on 0 või 1, mis on korrektne, aga mitte täpne. Ettepoole saab implementeerida täpsemad juhud kui vaja. *)
7792

7893
| _ -> failwith "TODO" (* Ei pea implementeerima kõiki operaatoreid, vaid ainult testideks vajalikud. *)

‎test/domain/intDomain_test.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,8 @@ struct
5252
assert_equal Top (Flat.eval_binary (Flat.of_int 2) Add Top);
5353
assert_equal Top (Flat.eval_binary Top Add (Flat.of_int 2));
5454
assert_equal Bot (Flat.eval_binary (Flat.of_int 2) Add Bot);
55-
assert_equal Bot (Flat.eval_binary Bot Add (Flat.of_int 2))
55+
assert_equal Bot (Flat.eval_binary Bot Add (Flat.of_int 2));
56+
assert_equal Bot (Flat.eval_binary Bot Add Top)
5657

5758
let test_exclude _ =
5859
assert_equal (Flat.of_int 5) (Flat.exclude 4 (Flat.of_int 5));

0 commit comments

Comments
 (0)