From b5d7c6c02d1be370fb63a8678bcf4b8be9e8474f Mon Sep 17 00:00:00 2001 From: Eric Patrizio Date: Wed, 15 Mar 2023 10:55:56 +0100 Subject: [PATCH 01/15] Init abstract interpretation (concrete domain) --- Makefile | 8 ++- abstract_interpreter.ml | 67 ++++++++++++++++++++ domain.ml | 46 ++++++++++++++ domain_concrete.ml | 132 ++++++++++++++++++++++++++++++++++++++++ main.ml | 20 ++++-- tests/t22.txt | 10 +++ tests/t23.txt | 8 +++ tests/t24.txt | 7 +++ tests/t25.txt | 4 ++ 9 files changed, 296 insertions(+), 6 deletions(-) create mode 100644 abstract_interpreter.ml create mode 100644 domain.ml create mode 100644 domain_concrete.ml create mode 100644 tests/t22.txt create mode 100644 tests/t23.txt create mode 100644 tests/t24.txt create mode 100644 tests/t25.txt diff --git a/Makefile b/Makefile index b8e57c4..551672c 100644 --- a/Makefile +++ b/Makefile @@ -15,8 +15,11 @@ all: ocamlc -c parser.ml; ocamlc -c lexer.ml; ocamlc -c typer.ml; + ocamlc -c domain.ml; + ocamlc -c domain_concrete.ml; + ocamlc -c abstract_interpreter.ml; ocamlc -c main.ml; - ocamlc -o $(EXE) utils.cmo ast.cmo compiler.cmo lexer.cmo parser.cmo typer.cmo main.cmo + ocamlc -o $(EXE) utils.cmo ast.cmo compiler.cmo lexer.cmo parser.cmo typer.cmo domain.cmo domain_concrete.cmo abstract_interpreter.cmo main.cmo clean: rm -rf *.cmo *.cmi lexer.ml parser.ml parser.mli $(EXE) @@ -36,6 +39,9 @@ compile_debug: compile_no_typing: @./$(EXE) --no-typing tests/$(S) +abs_inter_concrete: + @./$(EXE) --abs-inter-concrete tests/$(S) + vm: @$(VM) tests/build/bc_$(S) diff --git a/abstract_interpreter.ml b/abstract_interpreter.ml new file mode 100644 index 0000000..abd85be --- /dev/null +++ b/abstract_interpreter.ml @@ -0,0 +1,67 @@ +(* Abstract interpretation - interpreter by induction *) + +open Ast +open Domain + +module type INTERPRETER = +sig + val analyse_prog: prog -> unit +end + +module Interprete(D : DOMAIN) = +(struct + + type t = D.t + + let filter (a : t) (e : expr) (r : bool) : t = + let rec expr_handle a (*e,_*) e r = + match e with + | Eunop (_, Tbool, Unot, e) -> expr_handle a e (not r) + | Ebinop (_, Tbool, Band, e1, e2) -> + (if r then D.meet else D.join) (expr_handle a e1 r) (expr_handle a e2 r) + | Ebinop (_, Tbool, Bor, e1, e2) -> + (if r then D.join else D.meet) (expr_handle a e1 r) (expr_handle a e2 r) + | Ebinop (_, _, Beq, e1, e2) -> D.compare a e1 (if r then Beq else Bneq) e2 + | Ebinop (_, _, Bneq, e1, e2) -> D.compare a e1 (if r then Bneq else Beq) e2 + | Ebinop (_, _, Blt, e1, e2) -> D.compare a e1 (if r then Blt else Bgt) e2 + | Ebinop (_, _, Bgt, e1, e2) -> D.compare a e1 (if r then Bgt else Blt) e2 + | Ebinop (_, _, Ble, e1, e2) -> D.compare a e1 (if r then Ble else Bge) e2 + | Ebinop (_, _, Bge, e1, e2) -> D.compare a e1 (if r then Bge else Ble) e2 + | Ecst (_, Tbool, Cbool b) -> if b = r then a else D.bottom () + | _ -> D.bottom () + in + expr_handle a e r + + let rec eval_stmt (a : t) (s : stmt) : t = + let r = match s with + | Sassign (_, (Tint, v_name), e, s) -> eval_stmt (D.assign a v_name e) s + | Srefassign (_, (Tint, v_name), e) -> D.assign a v_name e + | Sprint (Eident (l, Tint, (Tint, s))) -> D.print a [s]; a + | Sprint (Ederef (l, Tint, (Tint, s))) -> D.print a [s]; a + | Sblock (Bstmt s) -> eval_stmt a s + | Sblock (Bseq_l (s, b)) -> eval_stmt (eval_stmt a s) (Sblock b) + | Sblock (Bseq_r (b, s)) -> eval_stmt (eval_stmt a (Sblock b)) s + | Sif (_, e, s1, s2) -> + let t = eval_stmt (filter a e true) s1 in + let f = eval_stmt (filter a e false) s2 in + D.join t f + | Swhile (_, e, b) -> + let rec fix (f:t -> t) (x:t) : t = + let fx = f x in + if D.subset fx x then fx + else fix f fx + in + let f x = D.join a (eval_stmt (filter x e true) (Sblock b)) in + let inv = fix f a in + filter inv e false + | Sfor (l,s1,e,s2,b) -> + let a1 = eval_stmt a s1 in + eval_stmt a1 (Swhile (l, e, (Bseq_r (b, s2)))) + | _ -> D.bottom () + in + r + + let analyse_prog (stmt : prog) : unit = + let _ = eval_stmt (D.init()) stmt in () + +end : INTERPRETER) diff --git a/domain.ml b/domain.ml new file mode 100644 index 0000000..6ddabd0 --- /dev/null +++ b/domain.ml @@ -0,0 +1,46 @@ +(* Abstract interpretation - Domains signature (abstract or concrete) *) + +open Ast + +module type DOMAIN = + sig + + (* abstract elements type *) + type t + + (* initial empty environment *) + val init: unit -> t + + (* empty set *) + val bottom: unit -> t + + (* add a variable in environment *) + val add_var: t -> string -> t + + (* remove a variable in environment *) + val del_var: t -> string -> t + + (* assign an integer expression to a variable *) + val assign: t -> string -> expr -> t + + (* filter environments *) + val compare: t -> expr -> binop -> expr -> t + + (* abstract join *) + val join: t -> t -> t + + (* abstract intersection *) + val meet: t -> t -> t + + (* abstract widening *) + val widen: t -> t -> t + + (* abstract element is included in another one *) + val subset: t -> t -> bool + + (* abstract element is the empty set *) + val is_bottom: t -> bool + + val print: t -> string list -> unit + + end diff --git a/domain_concrete.ml b/domain_concrete.ml new file mode 100644 index 0000000..5f7ab7e --- /dev/null +++ b/domain_concrete.ml @@ -0,0 +1,132 @@ +(* Abstract interpretation - Concrete execution domain *) + +open Ast +open Domain + +open Format + +module Concrete = (struct + + (* variables (strings) in a map *) + module Env = Map.Make(String) + + (* environment : we consider integer value *) + type env = int Env.t + + (* environments set *) + module EnvSet = + Set.Make + (struct + type t = env + let compare = Env.compare Int.compare + end) + + (* an element is a set of possible environments *) + type t = EnvSet.t + + (* a set of integer values *) + module ValSet = Set.Make + (struct + type t = int + let compare = Int.compare + end) + + let int_map (f : int -> int) (s : ValSet.t) : ValSet.t = + ValSet.fold (fun x acc -> ValSet.add (f x) acc) s ValSet.empty + + let int2_map (f: int -> int -> int) (s1:ValSet.t) (s2:ValSet.t) : ValSet.t = + ValSet.fold + (fun x1 acc -> + ValSet.fold + (fun x2 acc -> ValSet.add (f x1 x2) acc) s2 acc + ) s1 ValSet.empty + + let rec eval_expr (e : expr) (m : env) : ValSet.t = + match e with + | Ecst (_, Tint, Cint c) -> ValSet.singleton c + | Eident (_, Tint, (Tint, var)) -> ValSet.singleton (Env.find var m) + | Eref (_, Tint, e) -> eval_expr e m + | Ederef (_, Tint, (Tint, var)) -> ValSet.singleton (Env.find var m) + | Ebinop (_, Tint, Badd, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + int2_map (fun x y -> x + y) v1 v2 + | Ebinop (_, Tint, Bsub, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + int2_map (fun x y -> x - y) v1 v2 + | Ebinop (_, Tint, Bmul, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + int2_map (fun x y -> x * y) v1 v2 + | Ebinop (_, Tint, Bdiv, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + let v2 = ValSet.remove 0 v2 in int2_map (fun x y -> x / y) v1 v2 + | _ -> ValSet.empty + + let eval_compare (e1 : expr) (bop : binop) (e2 : expr) (m : env) : bool = + let f = + match bop with + | Beq -> Int.equal + | Bneq -> fun x y -> not (Int.equal x y) + | Blt -> fun x y -> x < y + | Ble -> fun x y -> x <= y + | Bgt -> fun x y -> x > y + | Bge -> fun x y -> x >= y + | _ -> fun _ _ -> false (* todo *) + in + let s1 = eval_expr e1 m and s2 = eval_expr e2 m in + ValSet.fold + (fun v1 acc -> + ValSet.fold + (fun v2 acc -> + (acc || (f v1 v2)) + ) s2 acc + ) s1 false + + let env_set_map f m = + EnvSet.fold (fun x acc -> EnvSet.add (f x) acc) m EnvSet.empty + + let init () = EnvSet.singleton Env.empty + + let bottom () = EnvSet.empty + + let add_var m v = env_set_map (Env.add v Int.zero) m + + let del_var m v = env_set_map (Env.remove v) m + + let assign m var e = + EnvSet.fold + (fun env acc -> + let s = eval_expr e env in + ValSet.fold + (fun v acc -> + EnvSet.add (Env.add var v env) acc + ) s acc + ) m EnvSet.empty + + let compare m e1 op e2 = + EnvSet.filter (fun env -> eval_compare e1 op e2 env) m + + let join m1 m2 = EnvSet.union m1 m2 + + let widen = join + + let meet m1 m2 = EnvSet.inter m1 m2 + + let subset m1 m2 = EnvSet.subset m1 m2 + + let is_bottom m = EnvSet.is_empty m + + let print m vars = + eprintf "{ "; + EnvSet.iter + (fun env -> + eprintf "["; + List.iter + (fun var -> + let v = Env.find var env in + eprintf "%s=%s;" var (Int.to_string v) + ) vars; + eprintf "]; " + ) m; + eprintf "}@." + +end: DOMAIN) diff --git a/main.ml b/main.ml index a9e1c37..07b8beb 100644 --- a/main.ml +++ b/main.ml @@ -2,6 +2,8 @@ open Format open Utils let no_typing = ref false +let abs_inter_concrete = ref false + let debug = ref false let in_file_name = ref "" @@ -9,20 +11,28 @@ let set_file s = in_file_name := s let options = [ "--no-typing", Arg.Set no_typing, " Compile without typing checks"; + "--abs-inter-concrete", Arg.Set abs_inter_concrete, " Abstract interpretation - concrete domain"; "--debug", Arg.Set debug, " Debug mode (ast printer)" ] let usage = "usage: ./c2mz [options] tests/bc_(test).txt" -let process source_code_file no_typing debug = +module ConcreteAnalysis = + Abstract_interpreter.Interprete(Domain_concrete.Concrete) + +let process source_code_file no_typing abs_inter_concrete debug = let ic = open_in source_code_file in let lexbuf = Lexing.from_channel ic in try let ast = Parser.prog Lexer.token lexbuf in close_in ic; - let ast = if not no_typing then Typer.typing ast else ast in - if debug then ast_printer ast; - Compiler.compile ast source_code_file + if abs_inter_concrete then + ConcreteAnalysis.analyse_prog (Typer.typing ast) + else ( + let ast = if not no_typing then Typer.typing ast else ast in + if debug then ast_printer ast; + Compiler.compile ast source_code_file + ) with | Lexer.Lexing_error c -> localisation (Lexing.lexeme_start_p lexbuf) source_code_file; @@ -52,4 +62,4 @@ let _ = Arg.usage options usage; exit 1 end; - process !in_file_name !no_typing !debug + process !in_file_name !no_typing !abs_inter_concrete !debug \ No newline at end of file diff --git a/tests/t22.txt b/tests/t22.txt new file mode 100644 index 0000000..d2175ab --- /dev/null +++ b/tests/t22.txt @@ -0,0 +1,10 @@ +let x = (ref 44) in +let y = (ref 2) in +begin + print x; + print y; + x := ((!x) - (!y)); + y := ((!y) + 8); + print x; + print y +end diff --git a/tests/t23.txt b/tests/t23.txt new file mode 100644 index 0000000..358894a --- /dev/null +++ b/tests/t23.txt @@ -0,0 +1,8 @@ +let x = (ref 10) in +begin + if ((!x) > (10+1)) then + x := ((!x) - 1) + else + x := ((!x) + 1); + print x +end diff --git a/tests/t24.txt b/tests/t24.txt new file mode 100644 index 0000000..9264ee8 --- /dev/null +++ b/tests/t24.txt @@ -0,0 +1,7 @@ +let x = (ref 0) in +begin + while ((!x) < 10) do + print x; + x := ((!x) + 1) + done +end diff --git a/tests/t25.txt b/tests/t25.txt new file mode 100644 index 0000000..98a1b02 --- /dev/null +++ b/tests/t25.txt @@ -0,0 +1,4 @@ +let x = (ref 0) in + for x:=0 ; ((!x)<10) ; x:=((!x)+1) do + print x + done From f7aa1b961e169038b9ca490b0ef6af384ab15c97 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 17 Mar 2023 14:49:22 +0100 Subject: [PATCH 02/15] Add line number in print function --- abstract_interpreter.ml | 4 ++-- domain.ml | 2 +- domain_concrete.ml | 3 ++- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/abstract_interpreter.ml b/abstract_interpreter.ml index abd85be..95f9ce4 100644 --- a/abstract_interpreter.ml +++ b/abstract_interpreter.ml @@ -36,8 +36,8 @@ module Interprete(D : DOMAIN) = let r = match s with | Sassign (_, (Tint, v_name), e, s) -> eval_stmt (D.assign a v_name e) s | Srefassign (_, (Tint, v_name), e) -> D.assign a v_name e - | Sprint (Eident (l, Tint, (Tint, s))) -> D.print a [s]; a - | Sprint (Ederef (l, Tint, (Tint, s))) -> D.print a [s]; a + | Sprint (Eident ((l,_), Tint, (Tint, s))) -> D.print l.pos_lnum a [s]; a + | Sprint (Ederef ((l,_), Tint, (Tint, s))) -> D.print l.pos_lnum a [s]; a | Sblock (Bstmt s) -> eval_stmt a s | Sblock (Bseq_l (s, b)) -> eval_stmt (eval_stmt a s) (Sblock b) | Sblock (Bseq_r (b, s)) -> eval_stmt (eval_stmt a (Sblock b)) s diff --git a/domain.ml b/domain.ml index 6ddabd0..d26996e 100644 --- a/domain.ml +++ b/domain.ml @@ -41,6 +41,6 @@ module type DOMAIN = (* abstract element is the empty set *) val is_bottom: t -> bool - val print: t -> string list -> unit + val print: int -> t -> string list -> unit end diff --git a/domain_concrete.ml b/domain_concrete.ml index 5f7ab7e..1c73262 100644 --- a/domain_concrete.ml +++ b/domain_concrete.ml @@ -115,7 +115,8 @@ module Concrete = (struct let is_bottom m = EnvSet.is_empty m - let print m vars = + let print lnum m vars = + eprintf "line %d: " lnum; eprintf "{ "; EnvSet.iter (fun env -> From e33f8249937797e3f75c5486ff9249cf1a77a8a7 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 17 Mar 2023 15:15:06 +0100 Subject: [PATCH 03/15] Add domain print_all function --- abstract_interpreter.ml | 1 + ast.ml | 1 + compiler.ml | 1 + domain.ml | 1 + domain_concrete.ml | 14 ++++++++++++++ lexer.mll | 1 + parser.mly | 3 ++- tests/t22.txt | 8 ++++---- typer.ml | 1 + utils.ml | 1 + 10 files changed, 27 insertions(+), 5 deletions(-) diff --git a/abstract_interpreter.ml b/abstract_interpreter.ml index 95f9ce4..4fb469b 100644 --- a/abstract_interpreter.ml +++ b/abstract_interpreter.ml @@ -38,6 +38,7 @@ module Interprete(D : DOMAIN) = | Srefassign (_, (Tint, v_name), e) -> D.assign a v_name e | Sprint (Eident ((l,_), Tint, (Tint, s))) -> D.print l.pos_lnum a [s]; a | Sprint (Ederef ((l,_), Tint, (Tint, s))) -> D.print l.pos_lnum a [s]; a + | Sprintall (l,_) -> D.print_all l.pos_lnum a; a | Sblock (Bstmt s) -> eval_stmt a s | Sblock (Bseq_l (s, b)) -> eval_stmt (eval_stmt a s) (Sblock b) | Sblock (Bseq_r (b, s)) -> eval_stmt (eval_stmt a (Sblock b)) s diff --git a/ast.ml b/ast.ml index b0e9a66..ce9eb3b 100644 --- a/ast.ml +++ b/ast.ml @@ -45,6 +45,7 @@ type stmt = | Swhile of loc * expr * block | Sfor of loc * stmt * expr * stmt * block | Sprint of expr + | Sprintall of loc | Sexit | Sskip diff --git a/compiler.ml b/compiler.ml index d4cd59f..21b907e 100644 --- a/compiler.ml +++ b/compiler.ml @@ -64,6 +64,7 @@ let rec compile_expr ?(label = "") e env k li = compile_expr e env 0 li @ labeled_inst ~label:("wcond"^sct) ("BRANCHIFNOT wdone"^sct) @ compile_block b env li @ compile_expr e env 0 li @ ["BRANCH wcond" ^ sct] @ labeled_inst ~label:("wdone"^sct) "" | Sfor (loc,s1,e,s2,b) -> compile_stmt s1 env li @ compile_stmt (Swhile (loc,e, Bseq_r (b,s2))) env li | Sprint e -> (compile_expr ~label:label e env 0 li) @ ["PRIM print"] + | Sprintall _ -> ["PRIM printall -- TODO"] | Sexit -> labeled_inst ~label:label ("STOP") @ li | Sskip -> labeled_inst ~label:label ("CONST 0") @ li diff --git a/domain.ml b/domain.ml index d26996e..22d2612 100644 --- a/domain.ml +++ b/domain.ml @@ -42,5 +42,6 @@ module type DOMAIN = val is_bottom: t -> bool val print: int -> t -> string list -> unit + val print_all: int -> t -> unit end diff --git a/domain_concrete.ml b/domain_concrete.ml index 1c73262..457e128 100644 --- a/domain_concrete.ml +++ b/domain_concrete.ml @@ -130,4 +130,18 @@ module Concrete = (struct ) m; eprintf "}@." + let print_all lnum m = + eprintf "line %d: " lnum; + eprintf "{ "; + EnvSet.iter + (fun env -> + eprintf "["; + Env.iter + (fun var v -> + eprintf "%s=%s;" var (Int.to_string v) + ) env; + eprintf "]; " + ) m; + eprintf "}@." + end: DOMAIN) diff --git a/lexer.mll b/lexer.mll index 845a3a8..e17de9f 100644 --- a/lexer.mll +++ b/lexer.mll @@ -62,6 +62,7 @@ rule token = parse | "or" { OR } | "not" { NOT } | "print" { PRINT } + | "print_all" { PRINT_ALL } | "array_size" { ARRAY_SIZE } | "exit" { EXIT } | "skip" { SKIP } diff --git a/parser.mly b/parser.mly index 60eac16..4a39100 100644 --- a/parser.mly +++ b/parser.mly @@ -11,7 +11,7 @@ %token CST %token LET IN REF BEGIN END IF THEN ELSE WHILE DO DONE FOR AND OR NOT -%token PRINT ARRAY_SIZE EXIT SKIP +%token PRINT PRINT_ALL ARRAY_SIZE EXIT SKIP %token EOF %token COMMA SEMICOLON EXCL LP RP LSQ RSQ LCU RCU %token EQUAL REF_EQUAL CMP_EQ CMP_NEQ CMP_LT CMP_LE CMP_GT CMP_GE @@ -44,6 +44,7 @@ stmt : | WHILE e=expr DO b=block DONE { Ast.Swhile (($startpos,$endpos), e, b) } | FOR s1=stmt SEMICOLON e=expr SEMICOLON s2=stmt DO b=block DONE { Ast.Sfor (($startpos,$endpos), s1, e, s2, b) } | PRINT e=expr { Ast.Sprint e } + | PRINT_ALL { Ast.Sprintall ($startpos,$endpos) } | EXIT { Ast.Sexit } | SKIP { Ast.Sskip } ; diff --git a/tests/t22.txt b/tests/t22.txt index d2175ab..3476fd4 100644 --- a/tests/t22.txt +++ b/tests/t22.txt @@ -1,10 +1,10 @@ let x = (ref 44) in let y = (ref 2) in begin - print x; - print y; + (* print x; *) + (* print y; *) + print_all; x := ((!x) - (!y)); y := ((!y) + 8); - print x; - print y + print_all end diff --git a/typer.ml b/typer.ml index 6ec9afd..046248a 100644 --- a/typer.ml +++ b/typer.ml @@ -244,6 +244,7 @@ and type_stmt env s = | _ -> error loc "not boolean type (if condition statement)" end end + | Sprintall loc -> Sprintall loc | Sexit -> Sexit | Sskip -> Sskip end diff --git a/utils.ml b/utils.ml index 6086938..3618898 100644 --- a/utils.ml +++ b/utils.ml @@ -121,6 +121,7 @@ let ast_printer ast_stmt = | Sfor (loc,s1,e,s2,b) -> eprintf "Stmt:for > "; loc_printer loc; stmt_printer s1; expr_printer e; stmt_printer s2; block_printer b | Sprint e -> eprintf "Stmt:print > "; expr_printer e + | Sprintall loc -> eprintf "Stmt:printall"; loc_printer loc | Sexit -> eprintf "Stmt:exit" | Sskip -> eprintf "Stmt:skip" end; From b25e79048690d8d3a1d65887c11481f79abcddc8 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 17 Mar 2023 17:44:53 +0100 Subject: [PATCH 04/15] Add rand ast expression --- ast.ml | 1 + compiler.ml | 3 ++- domain_concrete.ml | 8 +++++++- lexer.mll | 1 + parser.mly | 3 ++- tests/t70-0.txt | 2 ++ tests/t70-1.txt | 3 +++ tests/ty_err_70.txt | 2 ++ typer.ml | 5 +++++ utils.ml | 2 ++ 10 files changed, 27 insertions(+), 3 deletions(-) create mode 100644 tests/t70-0.txt create mode 100644 tests/t70-1.txt create mode 100644 tests/ty_err_70.txt diff --git a/ast.ml b/ast.ml index ce9eb3b..857928b 100644 --- a/ast.ml +++ b/ast.ml @@ -35,6 +35,7 @@ type expr = | Earray of loc * typ * expr list | Eaget of loc * typ * ident * expr | Easize of loc * typ * ident + | Erand of loc * typ * expr * expr type stmt = | Sassign of loc * ident * expr * stmt diff --git a/compiler.ml b/compiler.ml index 21b907e..408f165 100644 --- a/compiler.ml +++ b/compiler.ml @@ -46,7 +46,8 @@ let rec compile_expr ?(label = "") e env k li = compile_stmt (Sassign (loc, (ty1,tmp), e, Sif (loc, Ebinop (loc, ty1, Bge, (Eident (loc,ty2,(ty2,tmp))), (Easize (loc,Tint,(ty2,i)))), Sexit, Sskip))) env li @ compile_expr e env k li @ ["PUSH"] @ compile_expr (Eident (loc,ty2,(ty2,i))) env (k+1) li @ ["GETVECTITEM"] @ li | Easize (loc,_,(typ,i)) -> compile_expr (Eident (loc,typ,(typ,i))) env k li @ ["VECTLENGTH"] @ li - + | Erand (loc,typ,e1,e2) -> + (compile_expr e2 env k li) @ ["PUSH"] @ (compile_expr e1 env (k+1) li) @ ["PRIM rand -- TODO"] and compile_stmt ?(label = "") s env li = match s with | Sassign(loc,(_,i),e,s) -> diff --git a/domain_concrete.ml b/domain_concrete.ml index 457e128..f96a4f8 100644 --- a/domain_concrete.ml +++ b/domain_concrete.ml @@ -34,7 +34,7 @@ module Concrete = (struct let int_map (f : int -> int) (s : ValSet.t) : ValSet.t = ValSet.fold (fun x acc -> ValSet.add (f x) acc) s ValSet.empty - let int2_map (f: int -> int -> int) (s1:ValSet.t) (s2:ValSet.t) : ValSet.t = + let int2_map (f: int -> int -> int) (s1 : ValSet.t) (s2 : ValSet.t) : ValSet.t = ValSet.fold (fun x1 acc -> ValSet.fold @@ -59,6 +59,12 @@ module Concrete = (struct | Ebinop (_, Tint, Bdiv, e1, e2) -> let v1 = eval_expr e1 m and v2 = eval_expr e2 m in let v2 = ValSet.remove 0 v2 in int2_map (fun x y -> x / y) v1 v2 + | Erand (_, Tint, Ecst (_, Tint, Cint i1), Ecst (_, Tint, Cint i2)) -> + let rec rand_set v set = + if v > i2 then set + else rand_set (v+1) (ValSet.add v set) + in + rand_set i1 ValSet.empty | _ -> ValSet.empty let eval_compare (e1 : expr) (bop : binop) (e2 : expr) (m : env) : bool = diff --git a/lexer.mll b/lexer.mll index e17de9f..13cab5e 100644 --- a/lexer.mll +++ b/lexer.mll @@ -63,6 +63,7 @@ rule token = parse | "not" { NOT } | "print" { PRINT } | "print_all" { PRINT_ALL } + | "rand" { RAND } | "array_size" { ARRAY_SIZE } | "exit" { EXIT } | "skip" { SKIP } diff --git a/parser.mly b/parser.mly index 4a39100..65c0be2 100644 --- a/parser.mly +++ b/parser.mly @@ -11,7 +11,7 @@ %token CST %token LET IN REF BEGIN END IF THEN ELSE WHILE DO DONE FOR AND OR NOT -%token PRINT PRINT_ALL ARRAY_SIZE EXIT SKIP +%token PRINT PRINT_ALL RAND ARRAY_SIZE EXIT SKIP %token EOF %token COMMA SEMICOLON EXCL LP RP LSQ RSQ LCU RCU %token EQUAL REF_EQUAL CMP_EQ CMP_NEQ CMP_LT CMP_LE CMP_GT CMP_GE @@ -76,6 +76,7 @@ expr : | LCU l=expr_list RCU { Ast.Earray (($startpos,$endpos), Ast.Tunknown, l) } | i=IDENT LSQ e=expr RSQ { Ast.Eaget (($startpos,$endpos), Ast.Tunknown, (Ast.Tunknown, i), e) } | LP ARRAY_SIZE i=IDENT RP { Ast.Easize (($startpos,$endpos), Ast.Tunknown, (Ast.Tunknown, i)) } + | LP RAND e1=expr e2=expr RP { Ast.Erand (($startpos,$endpos), Ast.Tunknown, e1, e2) } ; expr_list : diff --git a/tests/t70-0.txt b/tests/t70-0.txt new file mode 100644 index 0000000..74297d8 --- /dev/null +++ b/tests/t70-0.txt @@ -0,0 +1,2 @@ +let r = (rand 3 9) in + print r diff --git a/tests/t70-1.txt b/tests/t70-1.txt new file mode 100644 index 0000000..0f3e347 --- /dev/null +++ b/tests/t70-1.txt @@ -0,0 +1,3 @@ +let r1 = (rand 3 9) in +let r2 = (rand 1 5) in + print_all diff --git a/tests/ty_err_70.txt b/tests/ty_err_70.txt new file mode 100644 index 0000000..f07e9a1 --- /dev/null +++ b/tests/ty_err_70.txt @@ -0,0 +1,2 @@ +let r = (rand 1 false) in (* error *) + print r diff --git a/typer.ml b/typer.ml index 046248a..46cd518 100644 --- a/typer.ml +++ b/typer.ml @@ -180,6 +180,11 @@ let rec type_expr env e = end with Not_found -> error loc ("unbound local var: " ^ i) end + | Erand (loc,_,e1,e2) -> + let ty1, ed1 = type_expr env e1 in + let ty2, ed2 = type_expr env e2 in + if ty1 == Tint && ty2 == Tint then Tint, Erand (loc,Tint,ed1,ed2) + else error loc "not integer type (> rand)" and type_stmt env s = begin match s with diff --git a/utils.ml b/utils.ml index 3618898..e32f95a 100644 --- a/utils.ml +++ b/utils.ml @@ -102,6 +102,8 @@ let ast_printer ast_stmt = | Eaget (loc,typ,i,e) -> eprintf "Expr:array_get > "; loc_printer loc; type_printer typ; ident_printer i; expr_printer e | Easize (loc,typ,i) -> eprintf "Expr:array_size > "; loc_printer loc; type_printer typ; ident_printer i + | Erand (loc,typ,e1,e2) -> + eprintf "Expr:rand > "; loc_printer loc; type_printer typ; expr_printer e1; expr_printer e2 end; eprintf "@]" and expr_list_printer l = From 4127f3efde2afa768e38929baba1cac76ce2e479 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Mon, 20 Mar 2023 16:42:17 +0100 Subject: [PATCH 05/15] specific abstract interpretation print and printall functions --- abstract_interpreter.ml | 5 ++--- ast.ml | 3 ++- compiler.ml | 3 ++- domain.ml | 2 +- domain_concrete.ml | 8 ++------ lexer.mll | 3 ++- parser.mly | 5 +++-- tests/t22.txt | 10 ---------- tests/t23.txt | 8 -------- tests/t24.txt | 7 ------- tests/tai1-0.txt | 10 ++++++++++ tests/tai1-1.txt | 8 ++++++++ tests/tai1-2.txt | 7 +++++++ tests/{t25.txt => tai1-3.txt} | 2 +- tests/{t70-0.txt => tai2-0.txt} | 2 +- tests/{t70-1.txt => tai2-1.txt} | 2 +- tests/tai2-2.txt | 9 +++++++++ tests/ty_err_ai_1-0.txt | 2 ++ tests/{ty_err_70.txt => ty_err_ai_2-0.txt} | 2 +- tests/ty_err_ai_2-1.txt | 2 ++ typer.ml | 9 ++++++++- utils.ml | 3 ++- 22 files changed, 66 insertions(+), 46 deletions(-) delete mode 100644 tests/t22.txt delete mode 100644 tests/t23.txt delete mode 100644 tests/t24.txt create mode 100644 tests/tai1-0.txt create mode 100644 tests/tai1-1.txt create mode 100644 tests/tai1-2.txt rename tests/{t25.txt => tai1-3.txt} (81%) rename tests/{t70-0.txt => tai2-0.txt} (62%) rename tests/{t70-1.txt => tai2-1.txt} (76%) create mode 100644 tests/tai2-2.txt create mode 100644 tests/ty_err_ai_1-0.txt rename tests/{ty_err_70.txt => ty_err_ai_2-0.txt} (74%) create mode 100644 tests/ty_err_ai_2-1.txt diff --git a/abstract_interpreter.ml b/abstract_interpreter.ml index 4fb469b..3213bb0 100644 --- a/abstract_interpreter.ml +++ b/abstract_interpreter.ml @@ -36,9 +36,8 @@ module Interprete(D : DOMAIN) = let r = match s with | Sassign (_, (Tint, v_name), e, s) -> eval_stmt (D.assign a v_name e) s | Srefassign (_, (Tint, v_name), e) -> D.assign a v_name e - | Sprint (Eident ((l,_), Tint, (Tint, s))) -> D.print l.pos_lnum a [s]; a - | Sprint (Ederef ((l,_), Tint, (Tint, s))) -> D.print l.pos_lnum a [s]; a - | Sprintall (l,_) -> D.print_all l.pos_lnum a; a + | Sprint_ai ((l,_), (Tint, v_name)) -> D.print l.pos_lnum a v_name; a + | Sprintall_ai (l,_) -> D.print_all l.pos_lnum a; a | Sblock (Bstmt s) -> eval_stmt a s | Sblock (Bseq_l (s, b)) -> eval_stmt (eval_stmt a s) (Sblock b) | Sblock (Bseq_r (b, s)) -> eval_stmt (eval_stmt a (Sblock b)) s diff --git a/ast.ml b/ast.ml index 857928b..b428e09 100644 --- a/ast.ml +++ b/ast.ml @@ -46,7 +46,8 @@ type stmt = | Swhile of loc * expr * block | Sfor of loc * stmt * expr * stmt * block | Sprint of expr - | Sprintall of loc + | Sprint_ai of loc * ident + | Sprintall_ai of loc | Sexit | Sskip diff --git a/compiler.ml b/compiler.ml index 408f165..1c7061c 100644 --- a/compiler.ml +++ b/compiler.ml @@ -65,7 +65,8 @@ let rec compile_expr ?(label = "") e env k li = compile_expr e env 0 li @ labeled_inst ~label:("wcond"^sct) ("BRANCHIFNOT wdone"^sct) @ compile_block b env li @ compile_expr e env 0 li @ ["BRANCH wcond" ^ sct] @ labeled_inst ~label:("wdone"^sct) "" | Sfor (loc,s1,e,s2,b) -> compile_stmt s1 env li @ compile_stmt (Swhile (loc,e, Bseq_r (b,s2))) env li | Sprint e -> (compile_expr ~label:label e env 0 li) @ ["PRIM print"] - | Sprintall _ -> ["PRIM printall -- TODO"] + | Sprint_ai _ -> [] (* only for abstract interpretation statement *) + | Sprintall_ai _ -> [] (* "" *) | Sexit -> labeled_inst ~label:label ("STOP") @ li | Sskip -> labeled_inst ~label:label ("CONST 0") @ li diff --git a/domain.ml b/domain.ml index 22d2612..76533ae 100644 --- a/domain.ml +++ b/domain.ml @@ -41,7 +41,7 @@ module type DOMAIN = (* abstract element is the empty set *) val is_bottom: t -> bool - val print: int -> t -> string list -> unit + val print: int -> t -> string -> unit val print_all: int -> t -> unit end diff --git a/domain_concrete.ml b/domain_concrete.ml index f96a4f8..2fc3109 100644 --- a/domain_concrete.ml +++ b/domain_concrete.ml @@ -121,17 +121,13 @@ module Concrete = (struct let is_bottom m = EnvSet.is_empty m - let print lnum m vars = + let print lnum m var = eprintf "line %d: " lnum; eprintf "{ "; EnvSet.iter (fun env -> eprintf "["; - List.iter - (fun var -> - let v = Env.find var env in - eprintf "%s=%s;" var (Int.to_string v) - ) vars; + eprintf "%s=%s" var (Int.to_string (Env.find var env)); eprintf "]; " ) m; eprintf "}@." diff --git a/lexer.mll b/lexer.mll index 13cab5e..4184b79 100644 --- a/lexer.mll +++ b/lexer.mll @@ -62,7 +62,8 @@ rule token = parse | "or" { OR } | "not" { NOT } | "print" { PRINT } - | "print_all" { PRINT_ALL } + | "print_ai" { PRINT_AI } + | "printall_ai" { PRINT_ALL_AI } | "rand" { RAND } | "array_size" { ARRAY_SIZE } | "exit" { EXIT } diff --git a/parser.mly b/parser.mly index 65c0be2..63a9660 100644 --- a/parser.mly +++ b/parser.mly @@ -11,7 +11,7 @@ %token CST %token LET IN REF BEGIN END IF THEN ELSE WHILE DO DONE FOR AND OR NOT -%token PRINT PRINT_ALL RAND ARRAY_SIZE EXIT SKIP +%token PRINT PRINT_AI PRINT_ALL_AI RAND ARRAY_SIZE EXIT SKIP %token EOF %token COMMA SEMICOLON EXCL LP RP LSQ RSQ LCU RCU %token EQUAL REF_EQUAL CMP_EQ CMP_NEQ CMP_LT CMP_LE CMP_GT CMP_GE @@ -44,7 +44,8 @@ stmt : | WHILE e=expr DO b=block DONE { Ast.Swhile (($startpos,$endpos), e, b) } | FOR s1=stmt SEMICOLON e=expr SEMICOLON s2=stmt DO b=block DONE { Ast.Sfor (($startpos,$endpos), s1, e, s2, b) } | PRINT e=expr { Ast.Sprint e } - | PRINT_ALL { Ast.Sprintall ($startpos,$endpos) } + | PRINT_AI i=IDENT { Ast.Sprint_ai (($startpos,$endpos), (Ast.Tunknown, i)) } + | PRINT_ALL_AI { Ast.Sprintall_ai ($startpos,$endpos) } | EXIT { Ast.Sexit } | SKIP { Ast.Sskip } ; diff --git a/tests/t22.txt b/tests/t22.txt deleted file mode 100644 index 3476fd4..0000000 --- a/tests/t22.txt +++ /dev/null @@ -1,10 +0,0 @@ -let x = (ref 44) in -let y = (ref 2) in -begin - (* print x; *) - (* print y; *) - print_all; - x := ((!x) - (!y)); - y := ((!y) + 8); - print_all -end diff --git a/tests/t23.txt b/tests/t23.txt deleted file mode 100644 index 358894a..0000000 --- a/tests/t23.txt +++ /dev/null @@ -1,8 +0,0 @@ -let x = (ref 10) in -begin - if ((!x) > (10+1)) then - x := ((!x) - 1) - else - x := ((!x) + 1); - print x -end diff --git a/tests/t24.txt b/tests/t24.txt deleted file mode 100644 index 9264ee8..0000000 --- a/tests/t24.txt +++ /dev/null @@ -1,7 +0,0 @@ -let x = (ref 0) in -begin - while ((!x) < 10) do - print x; - x := ((!x) + 1) - done -end diff --git a/tests/tai1-0.txt b/tests/tai1-0.txt new file mode 100644 index 0000000..d1aeba5 --- /dev/null +++ b/tests/tai1-0.txt @@ -0,0 +1,10 @@ +let x = (ref 44) in +let y = (ref 2) in + begin + (* print_ai x; *) + (* print_ai y; *) + printall_ai; + x := ((!x) - (!y)); + y := ((!y) + 8); + printall_ai + end diff --git a/tests/tai1-1.txt b/tests/tai1-1.txt new file mode 100644 index 0000000..f82b857 --- /dev/null +++ b/tests/tai1-1.txt @@ -0,0 +1,8 @@ +let x = (ref 10) in + begin + if ((!x) > (10+1)) then + x := ((!x) - 1) + else + x := ((!x) + 1); + print_ai x + end diff --git a/tests/tai1-2.txt b/tests/tai1-2.txt new file mode 100644 index 0000000..120b929 --- /dev/null +++ b/tests/tai1-2.txt @@ -0,0 +1,7 @@ +let x = (ref 0) in + begin + while ((!x) < 10) do + print_ai x; + x := ((!x) + 1) + done + end diff --git a/tests/t25.txt b/tests/tai1-3.txt similarity index 81% rename from tests/t25.txt rename to tests/tai1-3.txt index 98a1b02..58a99dd 100644 --- a/tests/t25.txt +++ b/tests/tai1-3.txt @@ -1,4 +1,4 @@ let x = (ref 0) in for x:=0 ; ((!x)<10) ; x:=((!x)+1) do - print x + print_ai x done diff --git a/tests/t70-0.txt b/tests/tai2-0.txt similarity index 62% rename from tests/t70-0.txt rename to tests/tai2-0.txt index 74297d8..9b2bae2 100644 --- a/tests/t70-0.txt +++ b/tests/tai2-0.txt @@ -1,2 +1,2 @@ let r = (rand 3 9) in - print r + print_ai r diff --git a/tests/t70-1.txt b/tests/tai2-1.txt similarity index 76% rename from tests/t70-1.txt rename to tests/tai2-1.txt index 0f3e347..e9f768a 100644 --- a/tests/t70-1.txt +++ b/tests/tai2-1.txt @@ -1,3 +1,3 @@ let r1 = (rand 3 9) in let r2 = (rand 1 5) in - print_all + printall_ai diff --git a/tests/tai2-2.txt b/tests/tai2-2.txt new file mode 100644 index 0000000..2eca6a3 --- /dev/null +++ b/tests/tai2-2.txt @@ -0,0 +1,9 @@ +let r = (rand 1 9) in +let x = (ref 0) in + begin + if (r > 5) then + x := 42 + else + x := 21; + printall_ai + end diff --git a/tests/ty_err_ai_1-0.txt b/tests/ty_err_ai_1-0.txt new file mode 100644 index 0000000..4b6a619 --- /dev/null +++ b/tests/ty_err_ai_1-0.txt @@ -0,0 +1,2 @@ +let b = false in + print_ai b (* error *) diff --git a/tests/ty_err_70.txt b/tests/ty_err_ai_2-0.txt similarity index 74% rename from tests/ty_err_70.txt rename to tests/ty_err_ai_2-0.txt index f07e9a1..2f2950e 100644 --- a/tests/ty_err_70.txt +++ b/tests/ty_err_ai_2-0.txt @@ -1,2 +1,2 @@ let r = (rand 1 false) in (* error *) - print r + print_ai r diff --git a/tests/ty_err_ai_2-1.txt b/tests/ty_err_ai_2-1.txt new file mode 100644 index 0000000..9bf864b --- /dev/null +++ b/tests/ty_err_ai_2-1.txt @@ -0,0 +1,2 @@ +let r = (rand 1 2) in + print_ai r_ub (* error *) diff --git a/typer.ml b/typer.ml index 46cd518..f089d36 100644 --- a/typer.ml +++ b/typer.ml @@ -249,7 +249,14 @@ and type_stmt env s = | _ -> error loc "not boolean type (if condition statement)" end end - | Sprintall loc -> Sprintall loc + | Sprint_ai(loc,(_,i)) -> begin + try + let typ = Tmap.find i env in + if typ == Tint then Sprint_ai(loc,(Tint,i)) + else error loc "not int ident (print_ai)" + with Not_found -> error loc ("unbound local var: " ^ i) + end + | Sprintall_ai loc -> Sprintall_ai loc | Sexit -> Sexit | Sskip -> Sskip end diff --git a/utils.ml b/utils.ml index e32f95a..ca4c96a 100644 --- a/utils.ml +++ b/utils.ml @@ -123,7 +123,8 @@ let ast_printer ast_stmt = | Sfor (loc,s1,e,s2,b) -> eprintf "Stmt:for > "; loc_printer loc; stmt_printer s1; expr_printer e; stmt_printer s2; block_printer b | Sprint e -> eprintf "Stmt:print > "; expr_printer e - | Sprintall loc -> eprintf "Stmt:printall"; loc_printer loc + | Sprint_ai (loc,i) -> eprintf "Stmt:print_ai > "; loc_printer loc; ident_printer i + | Sprintall_ai loc -> eprintf "Stmt:printall_ai > "; loc_printer loc | Sexit -> eprintf "Stmt:exit" | Sskip -> eprintf "Stmt:skip" end; From 96be7470ca764d3f2f3e7802e693d9d1e672480f Mon Sep 17 00:00:00 2001 From: epatrizio Date: Mon, 20 Mar 2023 17:05:18 +0100 Subject: [PATCH 06/15] Bug fix ebinop filter compare --- abstract_interpreter.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/abstract_interpreter.ml b/abstract_interpreter.ml index 3213bb0..8ade5be 100644 --- a/abstract_interpreter.ml +++ b/abstract_interpreter.ml @@ -23,10 +23,10 @@ module Interprete(D : DOMAIN) = (if r then D.join else D.meet) (expr_handle a e1 r) (expr_handle a e2 r) | Ebinop (_, _, Beq, e1, e2) -> D.compare a e1 (if r then Beq else Bneq) e2 | Ebinop (_, _, Bneq, e1, e2) -> D.compare a e1 (if r then Bneq else Beq) e2 - | Ebinop (_, _, Blt, e1, e2) -> D.compare a e1 (if r then Blt else Bgt) e2 - | Ebinop (_, _, Bgt, e1, e2) -> D.compare a e1 (if r then Bgt else Blt) e2 - | Ebinop (_, _, Ble, e1, e2) -> D.compare a e1 (if r then Ble else Bge) e2 - | Ebinop (_, _, Bge, e1, e2) -> D.compare a e1 (if r then Bge else Ble) e2 + | Ebinop (_, _, Blt, e1, e2) -> D.compare a e1 (if r then Blt else Bge) e2 + | Ebinop (_, _, Bgt, e1, e2) -> D.compare a e1 (if r then Bgt else Ble) e2 + | Ebinop (_, _, Ble, e1, e2) -> D.compare a e1 (if r then Ble else Bgt) e2 + | Ebinop (_, _, Bge, e1, e2) -> D.compare a e1 (if r then Bge else Blt) e2 | Ecst (_, Tbool, Cbool b) -> if b = r then a else D.bottom () | _ -> D.bottom () in From c48e2207e735cdbcf53ca2890596e2900d29c9ca Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 31 Mar 2023 11:50:59 +0200 Subject: [PATCH 07/15] Init constant domain (alpha version in progress) --- Makefile | 7 +- domain_constant.ml | 202 +++++++++++++++++++++++++++++++++++++++++++++ main.ml | 19 +++-- 3 files changed, 222 insertions(+), 6 deletions(-) create mode 100644 domain_constant.ml diff --git a/Makefile b/Makefile index 551672c..4b45d7a 100644 --- a/Makefile +++ b/Makefile @@ -17,9 +17,11 @@ all: ocamlc -c typer.ml; ocamlc -c domain.ml; ocamlc -c domain_concrete.ml; + ocamlc -c domain_constant.ml; ocamlc -c abstract_interpreter.ml; ocamlc -c main.ml; - ocamlc -o $(EXE) utils.cmo ast.cmo compiler.cmo lexer.cmo parser.cmo typer.cmo domain.cmo domain_concrete.cmo abstract_interpreter.cmo main.cmo + ocamlc -o $(EXE) utils.cmo ast.cmo compiler.cmo lexer.cmo parser.cmo typer.cmo \ + domain.cmo domain_concrete.cmo domain_constant.cmo abstract_interpreter.cmo main.cmo clean: rm -rf *.cmo *.cmi lexer.ml parser.ml parser.mli $(EXE) @@ -42,6 +44,9 @@ compile_no_typing: abs_inter_concrete: @./$(EXE) --abs-inter-concrete tests/$(S) +abs_inter_constant: + @./$(EXE) --abs-inter-constant tests/$(S) + vm: @$(VM) tests/build/bc_$(S) diff --git a/domain_constant.ml b/domain_constant.ml new file mode 100644 index 0000000..746c690 --- /dev/null +++ b/domain_constant.ml @@ -0,0 +1,202 @@ +(* Abstract interpretation - Constant domain *) + +open Ast +open Domain + +open Format + +module Constants = (struct + + type t_const = + | Cst of int + | BOT (* empty *) + | TOP (* all integers *) + + module Env = Map.Make(String) + + type env = t_const Env.t + + type t = + | Val of env + | BOTTOM + + let t_lift1 f (x : t_const) : t_const = + match x with + | BOT -> BOT + | TOP -> TOP + | Cst a -> Cst (f a) + + let t_lift2 f (x : t_const) (y : t_const) : t_const = + match x, y with + | BOT,_ | _,BOT -> BOT + | TOP,_ | _,TOP -> TOP + | Cst a, Cst b -> Cst (f a b) + + let t_join a b = + match a, b with + | BOT, x | x, BOT -> x + | Cst x, Cst y when x = y -> a + | _ -> TOP + + let t_meet a b = + match a, b with + | TOP, x | x, TOP -> x + | Cst x, Cst y when x = y -> a + | _ -> BOT + + let t_subset a b = + match a, b with + | BOT, _ | _, TOP -> true + | Cst x, Cst y -> x = y + | _ -> false + + let t_eq a b = + match a, b with + | BOT, _ | _, BOT -> BOT, BOT + | Cst va, Cst vb when va = vb -> a, b + | Cst _, Cst _ -> BOT, BOT + | TOP, x | x, TOP -> x, x + + let t_neq a b = + match a, b with + | Cst va, Cst vb when va != vb -> a, b + | Cst _, Cst _ -> BOT, BOT + | _, _ -> a, b + + let t_geq a b = + match a, b with + | Cst va, Cst vb when va >= vb -> a, b + | Cst _, Cst _ -> BOT, BOT + | _, _ -> a, b + + let t_gt a b = + match a, b with + | Cst va, Cst vb when va > vb -> a, b + | Cst _, Cst _ -> BOT, BOT + | _, _ -> a, b + + let t_leq a b = + let b', a' = t_geq b a in a', b' + + let t_lt a b = + let b', a' = t_gt b a in a', b' + + let t_print a = + match a with + | BOT -> eprintf "⊥" + | TOP -> eprintf "⊤" + | Cst x -> eprintf "{%s}" (Int.to_string x) + + let rec eval_expr (e : expr) (m : env) : t_const = + match e with + | Ecst (_, Tint, Cint c) -> Cst c + | Eident (_, Tint, (Tint, var)) -> Env.find var m + | Eref (_, Tint, e) -> eval_expr e m + | Ederef (_, Tint, (Tint, var)) -> Env.find var m + | Ebinop (_, Tint, Badd, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + t_lift2 (fun x y -> x + y) v1 v2 + | Ebinop (_, Tint, Bsub, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + t_lift2 (fun x y -> x - y) v1 v2 + | Ebinop (_, Tint, Bmul, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + if v1 = Cst 0 || v2 = Cst 0 then Cst 0 + else t_lift2 (fun x y -> x * y) v1 v2 + | Ebinop (_, Tint, Bdiv, e1, e2) -> + let v1 = eval_expr e1 m and v2 = eval_expr e2 m in + if v2 = Cst 0 then BOT + else t_lift2 (fun x y -> x / y) v1 v2 + | Erand (_, Tint, Ecst (_, Tint, Cint i1), Ecst (_, Tint, Cint i2)) -> + if i1 = i2 then Cst i1 + else if i1 < i2 then TOP + else BOT + | _ -> BOT + + let eval_compare (e1 : expr) (bop : binop) (e2 : expr) (m : env) : bool = + let f = + match bop with + | Beq -> t_eq + | Bneq -> t_neq + | Bgt -> t_gt + | Bge -> t_geq + | Blt -> t_lt + | Ble -> t_leq + | _ -> assert false + in + let s1 = eval_expr e1 m and s2 = eval_expr e2 m in + false + (* f s1 s2 *) + (* todo *) + + let init () = Val Env.empty + + let bottom () = BOTTOM + + let add_var m v = + match m with + | BOTTOM -> BOTTOM + | Val m -> Val (Env.add v (Cst 0) m) + + let del_var m v = + match m with + | BOTTOM -> BOTTOM + | Val m -> Val (Env.remove v m) + + let assign m v e = + match m with + | BOTTOM -> BOTTOM + | Val m -> + let c = eval_expr e m in + if c = BOT then BOTTOM + else Val (Env.add v c m) + + let compare m e1 op e2 = m (* todo *) + (* Env.filter (fun _ env -> eval_compare e1 op e2 env) m *) + + let join m1 m2 = + match m1, m2 with + | BOTTOM, x | x, BOTTOM -> x + | Val m, Val n -> Val (Env.union (fun k a b -> Some (t_join a b)) m n) (* todo *) + + let widen = join + + let meet m1 m2 = + match m1, m2 with + | BOTTOM, x | x, BOTTOM -> BOTTOM + | Val m, Val n -> Val (Env.union (fun _ a b -> Some (t_meet a b)) m n) (* todo *) + + let subset m1 m2 = + match m1, m2 with + | BOTTOM, _ -> true + | _, BOTTOM -> false + | Val m, Val n -> false (* Env.union (fun _ a b -> Some (t_subset a b)) m n *) (* todo *) + + let is_bottom m = + m = BOTTOM + + let print lnum m var = + eprintf "line %d: " lnum; + match m with + | BOTTOM -> eprintf "⊥" + | Val m -> + eprintf "["; + let v = Env.find var m in t_print v; + eprintf "]@." + + let print_all lnum m = + eprintf "line %d: " lnum; + match m with + | BOTTOM -> eprintf "⊥" + | Val m -> + eprintf "["; + let first = ref true in + Env.iter ( + fun key v -> + if !first then first := false else eprintf ","; + eprintf " %s in " key; + t_print v + ) m; + eprintf "]@." + +end: DOMAIN) diff --git a/main.ml b/main.ml index 07b8beb..7c781c9 100644 --- a/main.ml +++ b/main.ml @@ -3,6 +3,7 @@ open Utils let no_typing = ref false let abs_inter_concrete = ref false +let abs_inter_constant = ref false let debug = ref false @@ -12,6 +13,7 @@ let set_file s = in_file_name := s let options = [ "--no-typing", Arg.Set no_typing, " Compile without typing checks"; "--abs-inter-concrete", Arg.Set abs_inter_concrete, " Abstract interpretation - concrete domain"; + "--abs-inter-constant", Arg.Set abs_inter_constant, " Abstract interpretation - constant domain"; "--debug", Arg.Set debug, " Debug mode (ast printer)" ] @@ -20,7 +22,10 @@ let usage = "usage: ./c2mz [options] tests/bc_(test).txt" module ConcreteAnalysis = Abstract_interpreter.Interprete(Domain_concrete.Concrete) -let process source_code_file no_typing abs_inter_concrete debug = +module ConstantAnalysis = + Abstract_interpreter.Interprete(Domain_constant.Constants) + +let process source_code_file no_typing abs_inter_concrete abs_inter_constant debug = let ic = open_in source_code_file in let lexbuf = Lexing.from_channel ic in try @@ -29,9 +34,13 @@ let process source_code_file no_typing abs_inter_concrete debug = if abs_inter_concrete then ConcreteAnalysis.analyse_prog (Typer.typing ast) else ( - let ast = if not no_typing then Typer.typing ast else ast in - if debug then ast_printer ast; - Compiler.compile ast source_code_file + if abs_inter_constant then + ConstantAnalysis.analyse_prog (Typer.typing ast) + else ( + let ast = if not no_typing then Typer.typing ast else ast in + if debug then ast_printer ast; + Compiler.compile ast source_code_file + ) ) with | Lexer.Lexing_error c -> @@ -62,4 +71,4 @@ let _ = Arg.usage options usage; exit 1 end; - process !in_file_name !no_typing !abs_inter_concrete !debug \ No newline at end of file + process !in_file_name !no_typing !abs_inter_concrete !abs_inter_constant !debug From f1231495e381bfef9eef952d8aea25d84568942e Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 31 Mar 2023 11:59:03 +0200 Subject: [PATCH 08/15] Add help rule --- Makefile | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Makefile b/Makefile index 4b45d7a..da10b92 100644 --- a/Makefile +++ b/Makefile @@ -32,6 +32,9 @@ clean_bc: check_grammar: menhir --list-errors parser.mly +help: + @./$(EXE) --help + compile: @./$(EXE) tests/$(S) From 9771887ff3e2fdfbbd5b36391a37c476cf49c4e8 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 14 Apr 2023 11:23:38 +0200 Subject: [PATCH 09/15] Constant domain (beta version) --- domain_constant.ml | 106 +++++++++++++++++++++++++++++++-------------- 1 file changed, 74 insertions(+), 32 deletions(-) diff --git a/domain_constant.ml b/domain_constant.ml index 746c690..c162db6 100644 --- a/domain_constant.ml +++ b/domain_constant.ml @@ -20,6 +20,8 @@ module Constants = (struct | Val of env | BOTTOM + exception Empty + let t_lift1 f (x : t_const) : t_const = match x with | BOT -> BOT @@ -86,35 +88,43 @@ module Constants = (struct | BOT -> eprintf "⊥" | TOP -> eprintf "⊤" | Cst x -> eprintf "{%s}" (Int.to_string x) - - let rec eval_expr (e : expr) (m : env) : t_const = + + type etree = + | E_binop of binop * etree * t_const * etree * t_const + | E_var of string * t_const + | E_cst of t_const + + let rec eval_expr (e : expr) (m : env) : etree * t_const = match e with - | Ecst (_, Tint, Cint c) -> Cst c - | Eident (_, Tint, (Tint, var)) -> Env.find var m + | Ecst (_, Tint, Cint c) -> + let tc = Cst c in E_cst tc, tc + | Eident (_, Tint, (Tint, var)) -> + let v = Env.find var m in E_var (var, v), v | Eref (_, Tint, e) -> eval_expr e m - | Ederef (_, Tint, (Tint, var)) -> Env.find var m + | Ederef (_, Tint, (Tint, var)) -> + let v = Env.find var m in E_var (var, v), v | Ebinop (_, Tint, Badd, e1, e2) -> - let v1 = eval_expr e1 m and v2 = eval_expr e2 m in - t_lift2 (fun x y -> x + y) v1 v2 + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + E_binop (Badd, et1, v1, et2, v2), t_lift2 (fun x y -> x + y) v1 v2 | Ebinop (_, Tint, Bsub, e1, e2) -> - let v1 = eval_expr e1 m and v2 = eval_expr e2 m in - t_lift2 (fun x y -> x - y) v1 v2 + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + E_binop (Bsub, et1, v1, et2, v2), t_lift2 (fun x y -> x - y) v1 v2 | Ebinop (_, Tint, Bmul, e1, e2) -> - let v1 = eval_expr e1 m and v2 = eval_expr e2 m in - if v1 = Cst 0 || v2 = Cst 0 then Cst 0 - else t_lift2 (fun x y -> x * y) v1 v2 + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + if v1 = Cst 0 || v2 = Cst 0 then E_cst (Cst 0), Cst 0 + else E_binop (Bmul, et1, v1, et2, v2), t_lift2 (fun x y -> x * y) v1 v2 | Ebinop (_, Tint, Bdiv, e1, e2) -> - let v1 = eval_expr e1 m and v2 = eval_expr e2 m in - if v2 = Cst 0 then BOT - else t_lift2 (fun x y -> x / y) v1 v2 + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + if v2 = Cst 0 then E_cst BOT, BOT + else E_binop (Bdiv, et1, v1, et2, v2), t_lift2 (fun x y -> x / y) v1 v2 | Erand (_, Tint, Ecst (_, Tint, Cint i1), Ecst (_, Tint, Cint i2)) -> - if i1 = i2 then Cst i1 - else if i1 < i2 then TOP - else BOT - | _ -> BOT + if i1 = i2 then E_cst (Cst i1), Cst i1 + else if i1 < i2 then E_cst TOP, TOP + else E_cst BOT, BOT + | _ -> E_cst BOT, BOT - let eval_compare (e1 : expr) (bop : binop) (e2 : expr) (m : env) : bool = - let f = + let apply_compare (e1 : expr) (bop : binop) (e2 : expr) (m : env) : env = + let f_comp = match bop with | Beq -> t_eq | Bneq -> t_neq @@ -124,10 +134,21 @@ module Constants = (struct | Ble -> t_leq | _ -> assert false in - let s1 = eval_expr e1 m and s2 = eval_expr e2 m in - false - (* f s1 s2 *) - (* todo *) + let rec refine (m : env) (et : etree) (tc : t_const) : env = + match et with + | E_binop (b, et1, tc1, et2, tc2) -> refine (refine m et1 tc1) et2 tc2 + | E_var (var, t) -> + let v = t_meet t tc in + if v = BOT then raise Empty; + Env.add var v m + | E_cst t -> + let v = t_meet t tc in + if v = BOT then raise Empty; + m + in + let et1, c1 = eval_expr e1 m and et2, c2 = eval_expr e2 m in + let cc1, cc2 = f_comp c1 c2 in + refine (refine m et1 cc1) et2 cc2 let init () = Val Env.empty @@ -147,30 +168,51 @@ module Constants = (struct match m with | BOTTOM -> BOTTOM | Val m -> - let c = eval_expr e m in + let _, c = eval_expr e m in if c = BOT then BOTTOM else Val (Env.add v c m) - let compare m e1 op e2 = m (* todo *) - (* Env.filter (fun _ env -> eval_compare e1 op e2 env) m *) + let compare m e1 op e2 = + match m with + | BOTTOM -> BOTTOM + | Val m -> + try Val (apply_compare e1 op e2 m) + with Empty -> BOTTOM let join m1 m2 = match m1, m2 with | BOTTOM, x | x, BOTTOM -> x - | Val m, Val n -> Val (Env.union (fun k a b -> Some (t_join a b)) m n) (* todo *) + | Val m, Val n -> + Val (Env.union (fun k a b -> Some (t_join a b)) m n) let widen = join let meet m1 m2 = match m1, m2 with - | BOTTOM, x | x, BOTTOM -> BOTTOM - | Val m, Val n -> Val (Env.union (fun _ a b -> Some (t_meet a b)) m n) (* todo *) + | BOTTOM, x | x, BOTTOM -> x (* BOTTOM, x ? *) + | Val m, Val n -> + try Val ( + Env.merge + (fun _k a b -> match a, b with + | Some a, Some b -> + let r = t_meet a b in + (if r = BOT then raise Empty; + Some r) + | _, _ -> None + ) m n) + with Empty -> BOTTOM let subset m1 m2 = match m1, m2 with | BOTTOM, _ -> true | _, BOTTOM -> false - | Val m, Val n -> false (* Env.union (fun _ a b -> Some (t_subset a b)) m n *) (* todo *) + | Val m, Val n -> + Env.fold ( + fun _ tc_m acc_m -> + Env.fold ( + fun _ tc_n acc_n -> acc_n || t_subset tc_m tc_n + ) n acc_m + ) m false let is_bottom m = m = BOTTOM From 851ace3d1abb46c5484bb021e8bd50ea16260a12 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Thu, 20 Apr 2023 17:27:24 +0200 Subject: [PATCH 10/15] Add some tests for constant domain --- tests/tai1-0.txt | 5 +++++ tests/tai1-1.txt | 5 +++++ tests/tai1-4.txt | 6 ++++++ tests/tai1-5.txt | 7 +++++++ tests/tai1-6.txt | 13 +++++++++++++ tests/tai2-3.txt | 8 ++++++++ tests/tai2-4.txt | 13 +++++++++++++ tests/tai2-5.txt | 6 ++++++ 8 files changed, 63 insertions(+) create mode 100644 tests/tai1-4.txt create mode 100644 tests/tai1-5.txt create mode 100644 tests/tai1-6.txt create mode 100644 tests/tai2-3.txt create mode 100644 tests/tai2-4.txt create mode 100644 tests/tai2-5.txt diff --git a/tests/tai1-0.txt b/tests/tai1-0.txt index d1aeba5..f53c815 100644 --- a/tests/tai1-0.txt +++ b/tests/tai1-0.txt @@ -6,5 +6,10 @@ let y = (ref 2) in printall_ai; x := ((!x) - (!y)); y := ((!y) + 8); + printall_ai; + x := ((!y) - (!x)); + y := ((!y) * 8); + printall_ai; + y := ((!y) / 2); printall_ai end diff --git a/tests/tai1-1.txt b/tests/tai1-1.txt index f82b857..1f38c8e 100644 --- a/tests/tai1-1.txt +++ b/tests/tai1-1.txt @@ -4,5 +4,10 @@ let x = (ref 10) in x := ((!x) - 1) else x := ((!x) + 1); + print_ai x; + if ((!x) > 10) then + x := ((!x) - 1) + else + x := ((!x) + 1); print_ai x end diff --git a/tests/tai1-4.txt b/tests/tai1-4.txt new file mode 100644 index 0000000..a65747a --- /dev/null +++ b/tests/tai1-4.txt @@ -0,0 +1,6 @@ +let x = (ref 0) in + begin + while ((!x) < 10) do (* infinite loop *) + print_ai x + done + end diff --git a/tests/tai1-5.txt b/tests/tai1-5.txt new file mode 100644 index 0000000..c64249c --- /dev/null +++ b/tests/tai1-5.txt @@ -0,0 +1,7 @@ +let x = (ref 0) in + begin + while ((rand 0 1) == 1) do (* non deterministic loop *) + print_ai x; + x := ((!x) + 1) + done + end diff --git a/tests/tai1-6.txt b/tests/tai1-6.txt new file mode 100644 index 0000000..77fb814 --- /dev/null +++ b/tests/tai1-6.txt @@ -0,0 +1,13 @@ +let i = (ref 0) in +let j = (ref 0) in + begin + while ((!i) < 5) do (* nested loops *) + begin + while ((!j) < (!i)) do + j := ((!j) + 1) + done; + i := ((!i) + 1) + end + done; + printall_ai + end diff --git a/tests/tai2-3.txt b/tests/tai2-3.txt new file mode 100644 index 0000000..4f3acb2 --- /dev/null +++ b/tests/tai2-3.txt @@ -0,0 +1,8 @@ +let r1 = (rand 1 5) in +let r2 = (rand 6 9) in +let r = (ref (r1+r2)) in + begin + printall_ai; + r := (r1 * 10); + print_ai r + end diff --git a/tests/tai2-4.txt b/tests/tai2-4.txt new file mode 100644 index 0000000..74e8a80 --- /dev/null +++ b/tests/tai2-4.txt @@ -0,0 +1,13 @@ +let x = (ref 0) in + begin + if (10 > (rand 1 5)) then + x := 1 + else + x := 2; + print_ai x; + if (10 > (rand 1 12)) then + x := 1 + else + x := 2; + print_ai x + end diff --git a/tests/tai2-5.txt b/tests/tai2-5.txt new file mode 100644 index 0000000..9b9a560 --- /dev/null +++ b/tests/tai2-5.txt @@ -0,0 +1,6 @@ +let x = (rand 1 5) in +let y = (rand 6 9) in + if ((x < y) and (1 == 2)) then + print_ai x + else + print_ai y From 53ec2fa72de8985d73dd9db60fc7cd428ee6282c Mon Sep 17 00:00:00 2001 From: epatrizio Date: Wed, 26 Apr 2023 11:16:12 +0200 Subject: [PATCH 11/15] Constant domain (refactoring - add abstraction level) --- Makefile | 5 +- domain_constant.ml | 238 ++++++++++++--------------------------------- domain_non_rel.ml | 159 ++++++++++++++++++++++++++++++ domain_value.ml | 35 +++++++ main.ml | 3 +- 5 files changed, 263 insertions(+), 177 deletions(-) create mode 100644 domain_non_rel.ml create mode 100644 domain_value.ml diff --git a/Makefile b/Makefile index da10b92..199a697 100644 --- a/Makefile +++ b/Makefile @@ -16,12 +16,15 @@ all: ocamlc -c lexer.ml; ocamlc -c typer.ml; ocamlc -c domain.ml; + ocamlc -c domain_value.ml; + ocamlc -c domain_non_rel.ml; ocamlc -c domain_concrete.ml; ocamlc -c domain_constant.ml; ocamlc -c abstract_interpreter.ml; ocamlc -c main.ml; ocamlc -o $(EXE) utils.cmo ast.cmo compiler.cmo lexer.cmo parser.cmo typer.cmo \ - domain.cmo domain_concrete.cmo domain_constant.cmo abstract_interpreter.cmo main.cmo + domain.cmo domain_value.cmo domain_non_rel.cmo domain_concrete.cmo domain_constant.cmo \ + abstract_interpreter.cmo main.cmo clean: rm -rf *.cmo *.cmi lexer.ml parser.ml parser.mli $(EXE) diff --git a/domain_constant.ml b/domain_constant.ml index c162db6..0268432 100644 --- a/domain_constant.ml +++ b/domain_constant.ml @@ -1,244 +1,132 @@ (* Abstract interpretation - Constant domain *) open Ast -open Domain +open Domain_value open Format module Constants = (struct - type t_const = + type t = | Cst of int | BOT (* empty *) | TOP (* all integers *) - module Env = Map.Make(String) + let top = TOP - type env = t_const Env.t + let bottom = BOT - type t = - | Val of env - | BOTTOM + let const c = Cst c - exception Empty + let rand x y = + if x = y then Cst x + else if x < y then TOP + else BOT - let t_lift1 f (x : t_const) : t_const = + let is_bottom x = + x = BOT + + let lift1 f (x : t) : t = match x with | BOT -> BOT | TOP -> TOP | Cst a -> Cst (f a) - let t_lift2 f (x : t_const) (y : t_const) : t_const = + let lift2 f (x : t) (y : t) : t = match x, y with | BOT,_ | _,BOT -> BOT | TOP,_ | _,TOP -> TOP | Cst a, Cst b -> Cst (f a b) - let t_join a b = + let add = lift2 (fun x y -> x + y) + + let sub = lift2 (fun x y -> x - y) + + let mul a b = + if a = Cst 0 || b = Cst 0 then Cst 0 + else lift2 (fun x y -> x * y) a b + + let div a b = + if b = Cst 0 then BOT + else lift2 (fun x y -> x / y) a b + + let unary a uop = + match uop with + | _ -> assert false + + let binary a b bop = + match bop with + | Badd -> add a b + | Bsub -> sub a b + | Bmul -> mul a b + | Bdiv -> div a b + | _ -> assert false + + let join a b = match a, b with | BOT, x | x, BOT -> x | Cst x, Cst y when x = y -> a | _ -> TOP - let t_meet a b = + let widen = join + + let meet a b = match a, b with | TOP, x | x, TOP -> x | Cst x, Cst y when x = y -> a | _ -> BOT - let t_subset a b = + let subset a b = match a, b with | BOT, _ | _, TOP -> true | Cst x, Cst y -> x = y | _ -> false - let t_eq a b = + let eq a b = match a, b with | BOT, _ | _, BOT -> BOT, BOT | Cst va, Cst vb when va = vb -> a, b | Cst _, Cst _ -> BOT, BOT | TOP, x | x, TOP -> x, x - let t_neq a b = + let neq a b = match a, b with | Cst va, Cst vb when va != vb -> a, b | Cst _, Cst _ -> BOT, BOT | _, _ -> a, b - let t_geq a b = + let geq a b = match a, b with | Cst va, Cst vb when va >= vb -> a, b | Cst _, Cst _ -> BOT, BOT | _, _ -> a, b - let t_gt a b = + let gt a b = match a, b with | Cst va, Cst vb when va > vb -> a, b | Cst _, Cst _ -> BOT, BOT | _, _ -> a, b - let t_leq a b = - let b', a' = t_geq b a in a', b' + let leq a b = + let b', a' = geq b a in a', b' + + let lt a b = + let b', a' = gt b a in a', b' - let t_lt a b = - let b', a' = t_gt b a in a', b' + let compare a b bop = + match bop with + | Beq -> eq a b + | Bneq -> neq a b + | Bge -> geq a b + | Bgt -> gt a b + | Ble -> leq a b + | Blt -> lt a b + | _ -> assert false - let t_print a = + let print a = match a with | BOT -> eprintf "⊥" | TOP -> eprintf "⊤" | Cst x -> eprintf "{%s}" (Int.to_string x) - type etree = - | E_binop of binop * etree * t_const * etree * t_const - | E_var of string * t_const - | E_cst of t_const - - let rec eval_expr (e : expr) (m : env) : etree * t_const = - match e with - | Ecst (_, Tint, Cint c) -> - let tc = Cst c in E_cst tc, tc - | Eident (_, Tint, (Tint, var)) -> - let v = Env.find var m in E_var (var, v), v - | Eref (_, Tint, e) -> eval_expr e m - | Ederef (_, Tint, (Tint, var)) -> - let v = Env.find var m in E_var (var, v), v - | Ebinop (_, Tint, Badd, e1, e2) -> - let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in - E_binop (Badd, et1, v1, et2, v2), t_lift2 (fun x y -> x + y) v1 v2 - | Ebinop (_, Tint, Bsub, e1, e2) -> - let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in - E_binop (Bsub, et1, v1, et2, v2), t_lift2 (fun x y -> x - y) v1 v2 - | Ebinop (_, Tint, Bmul, e1, e2) -> - let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in - if v1 = Cst 0 || v2 = Cst 0 then E_cst (Cst 0), Cst 0 - else E_binop (Bmul, et1, v1, et2, v2), t_lift2 (fun x y -> x * y) v1 v2 - | Ebinop (_, Tint, Bdiv, e1, e2) -> - let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in - if v2 = Cst 0 then E_cst BOT, BOT - else E_binop (Bdiv, et1, v1, et2, v2), t_lift2 (fun x y -> x / y) v1 v2 - | Erand (_, Tint, Ecst (_, Tint, Cint i1), Ecst (_, Tint, Cint i2)) -> - if i1 = i2 then E_cst (Cst i1), Cst i1 - else if i1 < i2 then E_cst TOP, TOP - else E_cst BOT, BOT - | _ -> E_cst BOT, BOT - - let apply_compare (e1 : expr) (bop : binop) (e2 : expr) (m : env) : env = - let f_comp = - match bop with - | Beq -> t_eq - | Bneq -> t_neq - | Bgt -> t_gt - | Bge -> t_geq - | Blt -> t_lt - | Ble -> t_leq - | _ -> assert false - in - let rec refine (m : env) (et : etree) (tc : t_const) : env = - match et with - | E_binop (b, et1, tc1, et2, tc2) -> refine (refine m et1 tc1) et2 tc2 - | E_var (var, t) -> - let v = t_meet t tc in - if v = BOT then raise Empty; - Env.add var v m - | E_cst t -> - let v = t_meet t tc in - if v = BOT then raise Empty; - m - in - let et1, c1 = eval_expr e1 m and et2, c2 = eval_expr e2 m in - let cc1, cc2 = f_comp c1 c2 in - refine (refine m et1 cc1) et2 cc2 - - let init () = Val Env.empty - - let bottom () = BOTTOM - - let add_var m v = - match m with - | BOTTOM -> BOTTOM - | Val m -> Val (Env.add v (Cst 0) m) - - let del_var m v = - match m with - | BOTTOM -> BOTTOM - | Val m -> Val (Env.remove v m) - - let assign m v e = - match m with - | BOTTOM -> BOTTOM - | Val m -> - let _, c = eval_expr e m in - if c = BOT then BOTTOM - else Val (Env.add v c m) - - let compare m e1 op e2 = - match m with - | BOTTOM -> BOTTOM - | Val m -> - try Val (apply_compare e1 op e2 m) - with Empty -> BOTTOM - - let join m1 m2 = - match m1, m2 with - | BOTTOM, x | x, BOTTOM -> x - | Val m, Val n -> - Val (Env.union (fun k a b -> Some (t_join a b)) m n) - - let widen = join - - let meet m1 m2 = - match m1, m2 with - | BOTTOM, x | x, BOTTOM -> x (* BOTTOM, x ? *) - | Val m, Val n -> - try Val ( - Env.merge - (fun _k a b -> match a, b with - | Some a, Some b -> - let r = t_meet a b in - (if r = BOT then raise Empty; - Some r) - | _, _ -> None - ) m n) - with Empty -> BOTTOM - - let subset m1 m2 = - match m1, m2 with - | BOTTOM, _ -> true - | _, BOTTOM -> false - | Val m, Val n -> - Env.fold ( - fun _ tc_m acc_m -> - Env.fold ( - fun _ tc_n acc_n -> acc_n || t_subset tc_m tc_n - ) n acc_m - ) m false - - let is_bottom m = - m = BOTTOM - - let print lnum m var = - eprintf "line %d: " lnum; - match m with - | BOTTOM -> eprintf "⊥" - | Val m -> - eprintf "["; - let v = Env.find var m in t_print v; - eprintf "]@." - - let print_all lnum m = - eprintf "line %d: " lnum; - match m with - | BOTTOM -> eprintf "⊥" - | Val m -> - eprintf "["; - let first = ref true in - Env.iter ( - fun key v -> - if !first then first := false else eprintf ","; - eprintf " %s in " key; - t_print v - ) m; - eprintf "]@." - -end: DOMAIN) +end: VALUE_DOMAIN) diff --git a/domain_non_rel.ml b/domain_non_rel.ml new file mode 100644 index 0000000..869301d --- /dev/null +++ b/domain_non_rel.ml @@ -0,0 +1,159 @@ +(* Abstract interpretation - Non relational domain *) + +open Ast +open Domain +open Domain_value + +open Format + +module NonRelational(D : VALUE_DOMAIN) = (struct + + module Env = Map.Make(String) + + type env = D.t Env.t + + type t = + | Val of env + | BOTTOM + + exception Empty + + type etree = + | E_binop of binop * etree * D.t * etree * D.t + | E_var of string * D.t + | E_cst of D.t + + let rec eval_expr (e : expr) (m : env) : etree * D.t = + match e with + | Ecst (_, Tint, Cint c) -> + let tc = D.const c in E_cst tc, tc + | Eident (_, Tint, (Tint, var)) -> + let v = Env.find var m in E_var (var, v), v + | Eref (_, Tint, e) -> eval_expr e m + | Ederef (_, Tint, (Tint, var)) -> + let v = Env.find var m in E_var (var, v), v + | Ebinop (_, Tint, Badd, e1, e2) -> + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + E_binop (Badd, et1, v1, et2, v2), D.binary v1 v2 Badd + | Ebinop (_, Tint, Bsub, e1, e2) -> + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + E_binop (Bsub, et1, v1, et2, v2), D.binary v1 v2 Bsub + | Ebinop (_, Tint, Bmul, e1, e2) -> + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + E_binop (Bmul, et1, v1, et2, v2), D.binary v1 v2 Bmul + | Ebinop (_, Tint, Bdiv, e1, e2) -> + let et1, v1 = eval_expr e1 m and et2, v2 = eval_expr e2 m in + E_binop (Bdiv, et1, v1, et2, v2), D.binary v1 v2 Bdiv + | Erand (_, Tint, Ecst (_, Tint, Cint i1), Ecst (_, Tint, Cint i2)) -> + let r = D.rand i1 i2 in E_cst r, r + | _ -> E_cst D.bottom, D.bottom + + let apply_compare (e1 : expr) (bop : binop) (e2 : expr) (m : env) : env = + let rec refine (m : env) (et : etree) (tc : D.t) : env = + match et with + | E_binop (b, et1, tc1, et2, tc2) -> refine (refine m et1 tc1) et2 tc2 + | E_var (var, t) -> + let v = D.meet t tc in + if D.is_bottom v then raise Empty; + Env.add var v m + | E_cst t -> + let v = D.meet t tc in + if D.is_bottom v then raise Empty; + m + in + let et1, c1 = eval_expr e1 m and et2, c2 = eval_expr e2 m in + let cc1, cc2 = D.compare c1 c2 bop in + refine (refine m et1 cc1) et2 cc2 + + let init () = Val Env.empty + + let bottom () = BOTTOM + + let add_var m v = + match m with + | BOTTOM -> BOTTOM + | Val m -> Val (Env.add v (D.const 0) m) + + let del_var m v = + match m with + | BOTTOM -> BOTTOM + | Val m -> Val (Env.remove v m) + + let assign m v e = + match m with + | BOTTOM -> BOTTOM + | Val m -> + let _, c = eval_expr e m in + if D.is_bottom c then BOTTOM + else Val (Env.add v c m) + + let compare m e1 op e2 = + match m with + | BOTTOM -> BOTTOM + | Val m -> + try Val (apply_compare e1 op e2 m) + with Empty -> BOTTOM + + let join m1 m2 = + match m1, m2 with + | BOTTOM, x | x, BOTTOM -> x + | Val m, Val n -> + Val (Env.union (fun k a b -> Some (D.join a b)) m n) + + let widen = join + + let meet m1 m2 = + match m1, m2 with + | BOTTOM, x | x, BOTTOM -> x (* BOTTOM, x ? *) + | Val m, Val n -> + try Val ( + Env.merge + (fun _k a b -> match a, b with + | Some a, Some b -> + let r = D.meet a b in + (if D.is_bottom r then raise Empty; + Some r) + | _, _ -> None + ) m n) + with Empty -> BOTTOM + + let subset m1 m2 = + match m1, m2 with + | BOTTOM, _ -> true + | _, BOTTOM -> false + | Val m, Val n -> + Env.fold ( + fun _ tc_m acc_m -> + Env.fold ( + fun _ tc_n acc_n -> acc_n || D.subset tc_m tc_n + ) n acc_m + ) m false + + let is_bottom m = + m = BOTTOM + + let print lnum m var = + eprintf "line %d: " lnum; + match m with + | BOTTOM -> eprintf "⊥" + | Val m -> + eprintf "["; + let v = Env.find var m in D.print v; + eprintf "]@." + + let print_all lnum m = + eprintf "line %d: " lnum; + match m with + | BOTTOM -> eprintf "⊥" + | Val m -> + eprintf "["; + let first = ref true in + Env.iter ( + fun key v -> + if !first then first := false else eprintf ","; + eprintf " %s in " key; + D.print v + ) m; + eprintf "]@." + +end : DOMAIN) diff --git a/domain_value.ml b/domain_value.ml new file mode 100644 index 0000000..5f67f0d --- /dev/null +++ b/domain_value.ml @@ -0,0 +1,35 @@ +(* Abstract interpretation - Value domain interface *) + +open Ast + +module type VALUE_DOMAIN = + sig + + (* abstract element type *) + type t + + (* unrestricted set *) + val top: t + + (* empty set *) + val bottom: t + val is_bottom: t -> bool + + (* constant *) + val const: int -> t + + (* interval *) + val rand: int -> int -> t + + (* operations *) + val join: t -> t -> t + val meet: t -> t -> t + val subset: t -> t -> bool + val widen: t -> t -> t + + val unary: t -> unop -> t + val binary: t -> t -> binop -> t + val compare: t -> t -> binop -> (t * t) + + val print: t -> unit +end diff --git a/main.ml b/main.ml index 7c781c9..2be62e7 100644 --- a/main.ml +++ b/main.ml @@ -23,7 +23,8 @@ module ConcreteAnalysis = Abstract_interpreter.Interprete(Domain_concrete.Concrete) module ConstantAnalysis = - Abstract_interpreter.Interprete(Domain_constant.Constants) + Abstract_interpreter.Interprete( + Domain_non_rel.NonRelational(Domain_constant.Constants)) let process source_code_file no_typing abs_inter_concrete abs_inter_constant debug = let ic = open_in source_code_file in From 083b9c5f4e4d56599d0e902f473debf93cb2b559 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Wed, 26 Apr 2023 15:28:37 +0200 Subject: [PATCH 12/15] Interval domain (beta version) --- Makefile | 6 +- domain_interval.ml | 220 +++++++++++++++++++++++++++++++++++++++++++++ main.ml | 20 +++-- 3 files changed, 240 insertions(+), 6 deletions(-) create mode 100644 domain_interval.ml diff --git a/Makefile b/Makefile index 199a697..3e6cf9a 100644 --- a/Makefile +++ b/Makefile @@ -20,11 +20,12 @@ all: ocamlc -c domain_non_rel.ml; ocamlc -c domain_concrete.ml; ocamlc -c domain_constant.ml; + ocamlc -c domain_interval.ml; ocamlc -c abstract_interpreter.ml; ocamlc -c main.ml; ocamlc -o $(EXE) utils.cmo ast.cmo compiler.cmo lexer.cmo parser.cmo typer.cmo \ domain.cmo domain_value.cmo domain_non_rel.cmo domain_concrete.cmo domain_constant.cmo \ - abstract_interpreter.cmo main.cmo + domain_interval.cmo abstract_interpreter.cmo main.cmo clean: rm -rf *.cmo *.cmi lexer.ml parser.ml parser.mli $(EXE) @@ -53,6 +54,9 @@ abs_inter_concrete: abs_inter_constant: @./$(EXE) --abs-inter-constant tests/$(S) +abs_inter_interval: + @./$(EXE) --abs-inter-interval tests/$(S) + vm: @$(VM) tests/build/bc_$(S) diff --git a/domain_interval.ml b/domain_interval.ml new file mode 100644 index 0000000..1367701 --- /dev/null +++ b/domain_interval.ml @@ -0,0 +1,220 @@ +(* Abstract interpretation - Interval domain *) + +open Ast +open Domain_value + +open Format + +module Intervals = (struct + + type bound = + | Int of int (* Z *) + | PINF (* +∞ *) + | MINF (* −∞ *) + + type t = + | Itv of bound * bound + | BOT + + let top = Itv (MINF, PINF) + + let bottom = BOT + + let const c = Itv (Int c, Int c) + + let rand x y = + if x <= y then Itv (Int x, Int y) + else BOT + + let is_bottom x = + x = BOT + + let lift1 f x = + match x with + | Itv (a, b) -> f a b + | BOT -> BOT + + let lift2 f x y = + match x, y with + | Itv (x1, x2), Itv (y1, y2) -> Itv (f x1 y1, f x2 y2) + | BOT, _ | _, BOT -> BOT + + (* bounds operations *) + + let bound_neg b = + match b with + | MINF -> PINF + | PINF -> MINF + | Int i -> Int (-i) + + let bound_add b1 b2 = + match b1, b2 with + | MINF,PINF | PINF,MINF -> invalid_arg "bound_add" (* (+∞) + (−∞) *) + | MINF,_ | _,MINF -> MINF + | PINF,_ | _,PINF -> PINF + | Int i, Int j -> Int (i + j) + + let bound_mul b1 b2 = + match b1, b2 with + | Int z, MINF | Int z, PINF | MINF, Int z | PINF, Int z when z = 0 -> Int 0 + | Int i, PINF | PINF, Int i when i > 0 -> PINF + | Int i, MINF | MINF, Int i when i > 0 -> MINF + | Int i, PINF | PINF, Int i when i < 0 -> MINF + | Int i, MINF | MINF, Int i when i < 0 -> PINF + | Int i, Int j -> Int (i * j) + | _, _ -> invalid_arg "bound_mul" + + let bound_div b1 b2 = + match b1, b2 with + | Int _, PINF | Int _, MINF -> Int 0 + | PINF, PINF -> Int 1 + | MINF, MINF -> Int 1 + | PINF, Int i when i > 0 -> PINF + | PINF, Int i when i < 0 -> MINF + | MINF, Int i when i > 0 -> MINF + | MINF, Int i when i < 0 -> PINF + | Int i, Int j -> Int (i / j) + | _, _ -> invalid_arg "bound_div" + + let bound_cmp b1 b2 = + match b1, b2 with + | MINF,MINF | PINF,PINF -> 0 + | MINF,_ | _,PINF -> -1 + | PINF,_ | _,MINF -> 1 + | Int i, Int j -> Int.compare i j + + let bound_min_list (l : bound list) : bound = + List.fold_left (fun acc e -> if bound_cmp acc e = -1 then acc else e) (List.hd l) l + + let bound_max_list (l : bound list) : bound = + List.fold_left (fun acc e -> if bound_cmp acc e = 1 then acc else e) (List.hd l) l + + let neg x = + lift1 (fun a b -> Itv (bound_neg b, bound_neg a)) x + + let add x y = + lift2 (fun a b -> bound_add a b) x y + + let sub x y = + lift2 (fun a b -> bound_add a b) x (neg y) + + let mul x y = + match x, y with + | _, BOT | BOT, _ -> BOT + | Itv (x1, x2), Itv (y1, y2) -> + let lb = [bound_mul x1 y1; bound_mul x1 y2; bound_mul x2 y1; bound_mul x2 y2] in + let b1 = bound_min_list lb in + let b2 = bound_max_list lb in + Itv (b1, b2) + + let div_aux x y = + match x, y with + | Itv (x1, x2), Itv (Int y1, y2) when y1 > 0 -> + let b1 = bound_min_list [bound_div x1 (Int y1); bound_div x1 y2] in + let b2 = bound_max_list [bound_div x2 (Int y1); bound_div x2 y2] in + Itv (b1, b2) + | Itv (x1, x2), Itv (y1, Int y2) when y2 < 0 -> + let b1 = bound_min_list [bound_div x2 y1; bound_div x2 (Int y2)] in + let b2 = bound_max_list [bound_div x1 y1; bound_div x1 (Int y2)] in + Itv (b1, b2) + | _, Itv (Int x, Int y) when x = 0 && y = 0 -> BOT + | _, _ -> BOT + + let join x y = + match x, y with + | BOT, i | i, BOT -> i + | Itv (x1, x2), Itv (y1, y2) -> Itv (bound_min_list [x1; y1], bound_max_list [x2; y2]) + + let meet x y = + match x, y with + | BOT, _ | _, BOT -> BOT + | Itv (x1, x2), Itv (y1, y2) -> Itv (bound_max_list [x1; y1], bound_min_list [x2; y2]) + + let widen x y = + match x, y with + | BOT, i | i, BOT -> i + | Itv (x1, x2), Itv (y1, y2) -> + let a = if bound_cmp x1 y1 <= 0 then x1 else MINF in + let b = if bound_cmp x2 y2 >= 0 then x2 else PINF in + Itv (a, b) + + let subset x y = + match x, y with + | BOT, _ -> true + | _, BOT -> false + | Itv (x1, x2), Itv (y1, y2) -> bound_cmp x1 y1 >= 0 && bound_cmp x2 y2 <= 0 + + let div x y = + match y with + | Itv (a, b) when bound_cmp a (Int 0)>=0 || bound_cmp b (Int 0)<=0 -> + div_aux x y + | _ -> + let y_pos = meet y (Itv (Int 1, PINF)) in + let y_min = meet y (Itv (MINF, Int (-1))) in + join (div_aux x y_pos) (div_aux x y_min) + + let eq x y = + let i = meet x y in i, i + + let geq x y = + match x, y with + | BOT, _ -> BOT, BOT + | _, BOT -> x, y + | Itv (_, x2), Itv (y1, _) when bound_cmp x2 y1 < 0 -> BOT, BOT + | Itv (x1, x2), Itv (y1, y2) -> Itv (bound_max_list [x1; y1], x2), Itv (y1, bound_min_list [x2; y2]) + + let gt x y = + match x, y with + | BOT, _ -> BOT, BOT + | _, BOT -> x, y + | Itv (_, x2), Itv (y1, _) when bound_cmp x2 y1 <= 0 -> BOT, BOT + | Itv (x1, x2), Itv (y1, y2) -> + let max = bound_max_list [x1; bound_add y1 (Int 1)] in + let min = bound_min_list [bound_add x2 (bound_neg (Int 1)); y2] in + Itv (max, x2), Itv (y1, min) + + let neq x y = + (* x != y <=> x>y OR x assert false + + let binary a b bop = + match bop with + | Badd -> add a b + | Bsub -> sub a b + | Bmul -> mul a b + | Bdiv -> div a b + | _ -> assert false + + let compare a b bop = + match bop with + | Beq -> eq a b + | Bneq -> neq a b + | Bge -> geq a b + | Bgt -> gt a b + | Ble -> leq a b + | Blt -> lt a b + | _ -> assert false + + let print x = + match x with + | Itv (Int a, Int b) -> eprintf "[%s;%s]" (Int.to_string a) (Int.to_string b) + | Itv (MINF, Int b) -> eprintf "[-∞;%s]" (Int.to_string b) + | Itv (Int a, PINF) -> eprintf "[%s;+∞]" (Int.to_string a) + | Itv (MINF, PINF) -> eprintf "[-∞;+∞]" + | Itv (PINF, _) -> eprintf "⊥" + | Itv (_, MINF) -> eprintf "⊥" + | BOT -> eprintf "⊥" + +end: VALUE_DOMAIN) diff --git a/main.ml b/main.ml index 2be62e7..d9ba19c 100644 --- a/main.ml +++ b/main.ml @@ -4,6 +4,7 @@ open Utils let no_typing = ref false let abs_inter_concrete = ref false let abs_inter_constant = ref false +let abs_inter_interval = ref false let debug = ref false @@ -14,6 +15,7 @@ let options = [ "--no-typing", Arg.Set no_typing, " Compile without typing checks"; "--abs-inter-concrete", Arg.Set abs_inter_concrete, " Abstract interpretation - concrete domain"; "--abs-inter-constant", Arg.Set abs_inter_constant, " Abstract interpretation - constant domain"; + "--abs-inter-interval", Arg.Set abs_inter_interval, " Abstract interpretation - interval domain"; "--debug", Arg.Set debug, " Debug mode (ast printer)" ] @@ -26,7 +28,11 @@ module ConstantAnalysis = Abstract_interpreter.Interprete( Domain_non_rel.NonRelational(Domain_constant.Constants)) -let process source_code_file no_typing abs_inter_concrete abs_inter_constant debug = +module IntervalAnalysis = + Abstract_interpreter.Interprete( + Domain_non_rel.NonRelational(Domain_interval.Intervals)) + +let process source_code_file no_typing abs_inter_concrete abs_inter_constant abs_inter_interval debug = let ic = open_in source_code_file in let lexbuf = Lexing.from_channel ic in try @@ -38,9 +44,13 @@ let process source_code_file no_typing abs_inter_concrete abs_inter_constant deb if abs_inter_constant then ConstantAnalysis.analyse_prog (Typer.typing ast) else ( - let ast = if not no_typing then Typer.typing ast else ast in - if debug then ast_printer ast; - Compiler.compile ast source_code_file + if abs_inter_interval then + IntervalAnalysis.analyse_prog (Typer.typing ast) + else ( + let ast = if not no_typing then Typer.typing ast else ast in + if debug then ast_printer ast; + Compiler.compile ast source_code_file + ) ) ) with @@ -72,4 +82,4 @@ let _ = Arg.usage options usage; exit 1 end; - process !in_file_name !no_typing !abs_inter_concrete !abs_inter_constant !debug + process !in_file_name !no_typing !abs_inter_concrete !abs_inter_constant !abs_inter_interval !debug From c4f7046ab04b2cb47f99b691dd598e3b944662fd Mon Sep 17 00:00:00 2001 From: epatrizio Date: Thu, 27 Apr 2023 16:05:35 +0200 Subject: [PATCH 13/15] Add abstract interpretation documentation --- README.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 0687dc9..2a73f4c 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,8 @@ Here is a compiler producing bytecode for a simplified implementation of the OCaml Virtual Machine, called Mini-ZAM. -*This project is part of the Advanced Compilation course of my professional training at Sorbonne University (2022).* +*This project is part of the Advanced Compilation course of my professional training at +Sorbonne University (2022 2023).* ## Technical stack / choices @@ -71,3 +72,19 @@ S=t0.txt make compile_debug ``` Then, you need a Mini-ZAM to interpret the generated bytecode. + +## Abstract interpretation + +Here is a short introduction to [abstract interpretation](https://en.wikipedia.org/wiki/Abstract_interpretation), +which is an advanced **static program analysis** technique. For example +**Abstract interpretation** allows to detect possible division by 0, or memory overflows. + +This implementation (a simple adaptation of a lesson on this pedagogical compiler), +represents the very beginning of a complete research field in computer science. +It allows to have a first idea and to see how it can be written. + +I only consider integer values on 3 different analyses: + +* Concrete analysis: `S=tai1-0.txt make abs_inter_concrete` +* Constants analysis: `S=tai1-0.txt make abs_inter_constant` +* Intervals analysis: `S=tai1-0.txt make abs_inter_interval` From 951d53a9404cd7c2e98e9dfba59247b2342535a7 Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 28 Apr 2023 08:16:12 +0200 Subject: [PATCH 14/15] Mini refacto --- domain_constant.ml | 12 ++++++------ domain_interval.ml | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/domain_constant.ml b/domain_constant.ml index 0268432..7088304 100644 --- a/domain_constant.ml +++ b/domain_constant.ml @@ -26,29 +26,29 @@ module Constants = (struct let is_bottom x = x = BOT - let lift1 f (x : t) : t = + let lift1 f x = match x with | BOT -> BOT | TOP -> TOP | Cst a -> Cst (f a) - let lift2 f (x : t) (y : t) : t = + let lift2 f x y = match x, y with | BOT,_ | _,BOT -> BOT | TOP,_ | _,TOP -> TOP | Cst a, Cst b -> Cst (f a b) - let add = lift2 (fun x y -> x + y) + let add = lift2 Int.add - let sub = lift2 (fun x y -> x - y) + let sub = lift2 Int.sub let mul a b = if a = Cst 0 || b = Cst 0 then Cst 0 - else lift2 (fun x y -> x * y) a b + else lift2 Int.mul a b let div a b = if b = Cst 0 then BOT - else lift2 (fun x y -> x / y) a b + else lift2 Int.div a b let unary a uop = match uop with diff --git a/domain_interval.ml b/domain_interval.ml index 1367701..fecd829 100644 --- a/domain_interval.ml +++ b/domain_interval.ml @@ -83,10 +83,10 @@ module Intervals = (struct | PINF,_ | _,MINF -> 1 | Int i, Int j -> Int.compare i j - let bound_min_list (l : bound list) : bound = + let bound_min_list l = List.fold_left (fun acc e -> if bound_cmp acc e = -1 then acc else e) (List.hd l) l - let bound_max_list (l : bound list) : bound = + let bound_max_list l = List.fold_left (fun acc e -> if bound_cmp acc e = 1 then acc else e) (List.hd l) l let neg x = From 2d21341c73f7deebbd99931489e9906c94dac7eb Mon Sep 17 00:00:00 2001 From: epatrizio Date: Fri, 28 Apr 2023 08:18:04 +0200 Subject: [PATCH 15/15] Add fix point with widening --- abstract_interpreter.ml | 10 +++++----- domain_non_rel.ml | 8 ++++++-- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/abstract_interpreter.ml b/abstract_interpreter.ml index 8ade5be..38d68ba 100644 --- a/abstract_interpreter.ml +++ b/abstract_interpreter.ml @@ -46,13 +46,13 @@ module Interprete(D : DOMAIN) = let f = eval_stmt (filter a e false) s2 in D.join t f | Swhile (_, e, b) -> - let rec fix (f:t -> t) (x:t) : t = - let fx = f x in + let rec fix (f:(t -> t -> t) -> t -> t) (op:t -> t -> t) (x:t) (i:int) : t = + let fx = f op x in if D.subset fx x then fx - else fix f fx + else fix f (if i < 3 then D.join else D.widen) fx (i+1) (* widening after 3 iterations *) in - let f x = D.join a (eval_stmt (filter x e true) (Sblock b)) in - let inv = fix f a in + let f op x = op a (eval_stmt (filter x e true) (Sblock b)) in + let inv = fix f D.join a 0 in filter inv e false | Sfor (l,s1,e,s2,b) -> let a1 = eval_stmt a s1 in diff --git a/domain_non_rel.ml b/domain_non_rel.ml index 869301d..8f5f502 100644 --- a/domain_non_rel.ml +++ b/domain_non_rel.ml @@ -98,9 +98,13 @@ module NonRelational(D : VALUE_DOMAIN) = (struct match m1, m2 with | BOTTOM, x | x, BOTTOM -> x | Val m, Val n -> - Val (Env.union (fun k a b -> Some (D.join a b)) m n) + Val (Env.union (fun _ a b -> Some (D.join a b)) m n) - let widen = join + let widen m1 m2 = + match m1, m2 with + | BOTTOM, x | x, BOTTOM -> x + | Val m, Val n -> + Val (Env.union (fun _ a b -> Some (D.widen a b)) m n) let meet m1 m2 = match m1, m2 with