CHB:abstract when assigning volatile global variables

Author: sipma

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -2368,6 +2368,22 @@ object (self)
               rhs
          | _ -> rhs in
 
+       let is_rhs_volatile =
+         let rhsvars = Xprt.variables_in_expr rhs in
+         List.exists (fun v ->
+             if self#f#env#is_global_variable v then
+               TR.tfold_default
+                 (fun gvaddr ->
+                   if memmap#has_location gvaddr then
+                     let gloc = memmap#get_location gvaddr in
+                     gloc#is_volatile
+                   else
+                     false)
+                 false
+                 (self#f#env#get_global_variable_address v)
+             else
+               false) rhsvars in
+
        if self#f#env#is_global_variable lhs then
          let _ =
            log_diagnostics_result
@@ -2377,6 +2393,15 @@ object (self)
              ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs)] in
          [ABSTRACT_VARS [lhs]]
 
+       else if is_rhs_volatile then
+         let _ =
+           log_diagnostics_result
+             ~msg:(p2s self#l#toPretty)
+             ~tag:("get_assign_cmds_r: abstract volatile assignment")
+             __FILE__ __LINE__
+             ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs)] in
+         [ABSTRACT_VARS [lhs]]
+
        else
          let rhs =
            (* if rhs is a composite symbolic expression, create a new variable

CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml

@@ -157,6 +157,8 @@ object (self)
     | Ok ty -> is_scalar ty
     | _ -> false
 
+  method is_volatile: bool = BCHBCTypeUtil.is_volatile self#btype
+
   method is_typed: bool = not (btype_equal self#btype t_unknown)
 
   method size: int option = grec.gloc_size

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -4398,6 +4398,7 @@ class type global_location_int =
     method address: doubleword_int
     method btype: btype_t
     method size: int option
+    method is_volatile: bool
     method is_readonly: bool
     method is_initialized: bool
     method is_typed: bool

CodeHawk/CHB/bchlib/bCHSystemSettings.ml

@@ -116,10 +116,10 @@ let _ =
       ("BL-sig-rv", "enable");
       ("BXLR-sig-rv", "enable");
       ("LDR-array", "enable");
-      ("LDR-memop-tc", "enable");
+      ("LDR-memop-tc", "disable");
       ("LDR-stack-addr", "enable");
       ("LDR-struct-field", "enable");
-      ("LDRH-memop-tc", "enable");
+      ("LDRH-memop-tc", "disable");
       ("POP-sig-rv", "enable");
       ("STR-memop-tc", "enable")
     ]

CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml

@@ -1715,8 +1715,8 @@ object (self)
          (regvar_type_introduction "UXTH" rd);
          (regvar_linked_to_exit "UXTH" rd);
 
-         (let opttc = mk_btype_constraint rdtypevar t_short in
-          let rule = "UBFX-def-lhs" in
+         (let opttc = mk_btype_constraint rdtypevar t_ushort in
+          let rule = "UXTH-def-lhs" in
           (match opttc with
            | Some tc ->
               if fndata#is_typing_rule_enabled iaddr rule then