From 041d492986faefbde14bdce9a53c6dfdc0651f6d Mon Sep 17 00:00:00 2001
From: Granahir2 <a1687516@gmail.com>
Date: Sat, 1 Jun 2024 19:29:10 +0200
Subject: [PATCH] Fixed up signs, less naive func support

---
 domains/sign.ml           | 23 ++++++++++++++++-------
 examples/sign/functions.c | 18 ++++++++++++++++++
 frontend/options.ml       |  2 +-
 iterator/iterator.ml      |  8 ++++++--
 scripts/test.sh           |  1 +
 5 files changed, 42 insertions(+), 10 deletions(-)
 create mode 100644 examples/sign/functions.c

diff --git a/domains/sign.ml b/domains/sign.ml
index fbf271c..6330d8b 100644
--- a/domains/sign.ml
+++ b/domains/sign.ml
@@ -38,15 +38,24 @@ module Signs : NAKED_VALUE_DOMAIN = struct
 		| AST_NOT_EQUAL -> raise NeedTop
 		| AST_LESS | AST_LESS_EQUAL -> if a == P || a == Z then P else raise NeedTop
 		| AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then N else raise NeedTop
-	let compare a b op = match op with
+	let rec compare a b op = match op with
 		| AST_EQUAL 	-> if a <> b then Z, Z else a, b
 		| AST_NOT_EQUAL -> if a == b && a == Z then raise Absurd else a, b
-		| AST_LESS | AST_LESS_EQUAL -> if b == N || b == Z then
-						(match a with | P -> Z | Z -> Z | N -> N), b
-						else a, b (*if b is P then we learn nothing*)
-		| AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then
-							a, (match b with | P -> Z | Z -> Z | N -> N)
-						     else a,b
+		| AST_LESS_EQUAL -> (match b with
+					| Z -> (match a with | P -> Z | Z -> Z | N -> N), b
+					| N -> (match a with
+						| P -> Z,Z
+						| N -> N,N
+						| Z -> Z,Z)
+					| P -> a,b)
+		| AST_LESS -> (match b with
+				| Z -> (match a with | P -> raise Absurd | Z -> raise Absurd | N -> N), b
+				| N -> (match a with
+					| P -> raise Absurd
+					| N -> N,N
+					| Z -> raise Absurd)
+				| P -> a,b)
+		| AST_GREATER_EQUAL | AST_GREATER -> let b',a' = compare b a (reverse op) in a', b'
 
 	let meet x y = match x,y with
 			|P, N | N, P -> raise Absurd
diff --git a/examples/sign/functions.c b/examples/sign/functions.c
new file mode 100644
index 0000000..a672441
--- /dev/null
+++ b/examples/sign/functions.c
@@ -0,0 +1,18 @@
+
+int abs(int x) {
+	if(x < 0) {
+		return -x;
+	} else {
+		return x;
+	}
+}
+
+void main() {
+	int x = rand(0,10);
+	int y = abs(x);
+	assert(y >= 0);
+	x = rand(-10, 10);
+	y = abs(x);
+	assert(y >= 0);
+}
+
diff --git a/frontend/options.ml b/frontend/options.ml
index 9c21226..7b20b11 100644
--- a/frontend/options.ml
+++ b/frontend/options.ml
@@ -30,7 +30,7 @@ let args = [
   "--dot-out", Set_string cfg_out,
     " Print the cfg in this file (default is cfg.dot)";
   "--domain", Set_string domain,
-    " Select the abstract domain (constants/interval)";
+    " Select the abstract domain (constants/interval/signs)";
 ] |> align
 
 let usage = "usage: ./analyzer.exe [options] filename.c"
diff --git a/iterator/iterator.ml b/iterator/iterator.ml
index 0dae579..4210e54 100644
--- a/iterator/iterator.ml
+++ b/iterator/iterator.ml
@@ -34,6 +34,7 @@ module Iterator (D : DOMAIN) = struct
 				func_state := NodeMap.add n (D.join s (node_abst n)) !func_state in
 
 			let rec iterate n = begin
+				(*Format.printf "@[<h 0> Handling node %i@]@ " n.node_id;*)
 				func_dirty := NodeSet.remove n !func_dirty;
 				let curr_abst = node_abst n in
 				let l = List.filter (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in begin
@@ -70,8 +71,11 @@ module Iterator (D : DOMAIN) = struct
 					func_args = [];
 					func_ret = None;
 					func_calls = []} D.init in
-			let x = List.hd cfg.cfg_funcs in (* we are ASSUMING main() is function 0*)
-			let _ = do_fun x init_st in
+			let rec do_main l = match l with
+				| x::_ when x.func_name = "main" -> do_fun x init_st
+				| _::q -> do_main q
+				| [] -> failwith "function main() not found" in
+			let _ = do_main cfg.cfg_funcs in
 			Format.printf "@]";
 			!failed_asserts
 		end
diff --git a/scripts/test.sh b/scripts/test.sh
index 89b8a50..1f8ca8d 100755
--- a/scripts/test.sh
+++ b/scripts/test.sh
@@ -265,6 +265,7 @@ treat_examples "constant" "Constants operations (I)" "--domain interval" ""
 treat_examples "interval" "Interval operations" "--domain interval" ""
 treat_examples "constant_loop" "Constants loops (I)" "--domain interval" ""
 treat_examples "interval_loop" "Interval loops" "--domain interval" ""
+treat_examples "sign" "Sign and misc." "--domain signs" ""
 echo "</table>"                                   >> $index_html
 echo "</body>"                                    >> $index_html
 echo "</html>"                                    >> $index_html